Theorem opexg 3937

Description: An ordered pair of sets is a set. (Contributed by Jim Kingdon, 11-Jan-2019.)

Assertion

Ref	Expression
opexg	⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → ⟨A, B⟩ ∈ V)

Proof of Theorem opexg

Step	Hyp	Ref	Expression
1		dfopg 3520	. 2 ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → ⟨A, B⟩ = {{A}, {A, B}})
2		elex 2542	. . . . 5 ⊢ (A ∈ 𝑉 → A ∈ V)
3		snexg 3909	. . . . 5 ⊢ (A ∈ V → {A} ∈ V)
4	2, 3	syl 14	. . . 4 ⊢ (A ∈ 𝑉 → {A} ∈ V)
5	4	adantr 261	. . 3 ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → {A} ∈ V)
6		elex 2542	. . . 4 ⊢ (B ∈ 𝑊 → B ∈ V)
7		prexg 3920	. . . 4 ⊢ ((A ∈ V ∧ B ∈ V) → {A, B} ∈ V)
8	2, 6, 7	syl2an 273	. . 3 ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → {A, B} ∈ V)
9		prexg 3920	. . 3 ⊢ (({A} ∈ V ∧ {A, B} ∈ V) → {{A}, {A, B}} ∈ V)
10	5, 8, 9	syl2anc 393	. 2 ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → {{A}, {A, B}} ∈ V)
11	1, 10	eqeltrd 2097	1 ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → ⟨A, B⟩ ∈ V)

Syntax hints:   → wi 4   ∧ wa 97   ∈ wcel 1375  Vcvv 2534  {csn 3349  {cpr 3350  ⟨cop 3352

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1364  ax-ie2 1365  ax-8 1377  ax-10 1378  ax-11 1379  ax-i12 1380  ax-bnd 1381  ax-4 1382  ax-14 1387  ax-17 1401  ax-i9 1405  ax-ial 1410  ax-i5r 1411  ax-ext 2005  ax-sep 3848  ax-pow 3900  ax-pr 3917

This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-nf 1330  df-sb 1629  df-clab 2010  df-cleq 2016  df-clel 2019  df-nfc 2150  df-v 2536  df-un 2898  df-in 2900  df-ss 2907  df-pw 3335  df-sn 3355  df-pr 3356  df-op 3358

This theorem is referenced by:  opex  3939  otexg  3940  fliftel1  5357  oprabid  5459  eloprabga  5512  op1st  5693  op2nd  5694  ot1stg  5699  ot2ndg  5700  ot3rdgg  5701  elxp6  5716  mpt2fvex  5749  algrflem  5770  mpt2xopoveq  5774  brtposg  5788  tfrlemisucaccv  5855  tfrlemibxssdm  5857  tfrlemibfn  5858  tfrlemi14d  5863  mulpipq2  6222  enq0breq  6277