Theorem opexg 4064

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

Assertion

Ref	Expression
opexg	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ ∈ V)

Proof of Theorem opexg

Step	Hyp	Ref	Expression
1		dfopg 3626	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ = {{𝐴}, {𝐴, 𝐵}})
2		elex 2631	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
3		snexg 4025	. . . . 5 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
4	2, 3	syl 14	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
5	4	adantr 271	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴} ∈ V)
6		elex 2631	. . . 4 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
7		prexg 4047	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
8	2, 6, 7	syl2an 284	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
9		prexg 4047	. . 3 ⊢ (({𝐴} ∈ V ∧ {𝐴, 𝐵} ∈ V) → {{𝐴}, {𝐴, 𝐵}} ∈ V)
10	5, 8, 9	syl2anc 404	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {{𝐴}, {𝐴, 𝐵}} ∈ V)
11	1, 10	eqeltrd 2165	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ ∈ V)

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1439  Vcvv 2620  {csn 3450  {cpr 3451  ⟨cop 3453

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3963  ax-pow 4015  ax-pr 4045

This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-v 2622  df-un 3004  df-in 3006  df-ss 3013  df-pw 3435  df-sn 3456  df-pr 3457  df-op 3459

This theorem is referenced by:  opex  4065  otexg  4066  opeliunxp  4506  opbrop  4530  relsnopg  4555  opswapg  4930  elxp4  4931  elxp5  4932  resfunexg  5532  fliftel  5586  fliftel1  5587  oprabid  5695  ovexg  5697  eloprabga  5749  op1st  5931  op2nd  5932  ot1stg  5937  ot2ndg  5938  ot3rdgg  5939  elxp6  5954  mpt2fvex  5987  algrflem  6008  algrflemg  6009  mpt2xopoveq  6019  brtposg  6033  tfr0dm  6101  tfrlemisucaccv  6104  tfrlemibxssdm  6106  tfrlemibfn  6107  tfrlemi14d  6112  tfr1onlemsucaccv  6120  tfr1onlembxssdm  6122  tfr1onlembfn  6123  tfr1onlemres  6128  tfrcllemsucaccv  6133  tfrcllembxssdm  6135  tfrcllembfn  6136  tfrcllemres  6141  fnfi  6700  djulclb  6801  djur  6811  1stinl  6819  2ndinl  6820  1stinr  6821  2ndinr  6822  mulpipq2  6991  enq0breq  7056  addvalex  7442  peano2nnnn  7451  axcnre  7477  frec2uzrdg  9877  frecuzrdg0  9881  frecuzrdgg  9884  frecuzrdg0t  9890  zfz1isolem1  10306  eucalgval2  11374  crth  11539  phimullem  11540  setsvala  11586  setsex  11587  setsfun  11590  setsfun0  11591  setsresg  11593  setscom  11595  strslfv  11599  setsslid  11605  strle1g  11645  1strbas  11654  2strbasg  11656  2stropg  11657  2strbas1g  11659  2strop1g  11660  rngbaseg  11671  rngplusgg  11672  rngmulrg  11673  srngbased  11678  srngplusgd  11679  srngmulrd  11680  srnginvld  11681  lmodbased  11689  lmodplusgd  11690  lmodscad  11691  lmodvscad  11692  ipsbased  11697  ipsaddgd  11698  ipsmulrd  11699  ipsscad  11700  ipsvscad  11701  ipsipd  11702  topgrpbasd  11707  topgrpplusgd  11708  topgrptsetd  11709