Theorem opexg 4261

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 3806	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ = {{𝐴}, {𝐴, 𝐵}})
2		elex 2774	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
3		snexg 4217	. . . . 5 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
4	2, 3	syl 14	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
5	4	adantr 276	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴} ∈ V)
6		elex 2774	. . . 4 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
7		prexg 4244	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
8	2, 6, 7	syl2an 289	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
9		prexg 4244	. . 3 ⊢ (({𝐴} ∈ V ∧ {𝐴, 𝐵} ∈ V) → {{𝐴}, {𝐴, 𝐵}} ∈ V)
10	5, 8, 9	syl2anc 411	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {{𝐴}, {𝐴, 𝐵}} ∈ V)
11	1, 10	eqeltrd 2273	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ ∈ V)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  Vcvv 2763  {csn 3622  {cpr 3623  ⟨cop 3625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4151  ax-pow 4207  ax-pr 4242

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631

This theorem is referenced by:  opex  4262  otexg  4263  opeliunxp  4718  opbrop  4742  relsnopg  4767  opswapg  5156  elxp4  5157  elxp5  5158  resfunexg  5783  fliftel  5840  fliftel1  5841  oprabid  5954  ovexg  5956  eloprabga  6009  op1st  6204  op2nd  6205  ot1stg  6210  ot2ndg  6211  ot3rdgg  6212  elxp6  6227  mpofvex  6263  algrflem  6287  algrflemg  6288  mpoxopoveq  6298  brtposg  6312  tfr0dm  6380  tfrlemisucaccv  6383  tfrlemibxssdm  6385  tfrlemibfn  6386  tfrlemi14d  6391  tfr1onlemsucaccv  6399  tfr1onlembxssdm  6401  tfr1onlembfn  6402  tfr1onlemres  6407  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllembfn  6415  tfrcllemres  6420  fnfi  7002  djulclb  7121  inl11  7131  1stinl  7140  2ndinl  7141  1stinr  7142  2ndinr  7143  mulpipq2  7438  enq0breq  7503  addvalex  7911  peano2nnnn  7920  axcnre  7948  frec2uzrdg  10501  frecuzrdg0  10505  frecuzrdgg  10508  frecuzrdg0t  10514  zfz1isolem1  10932  eucalgval2  12221  crth  12392  phimullem  12393  ennnfonelemp1  12623  setsvala  12709  setsex  12710  setsfun  12713  setsfun0  12714  setsresg  12716  setscom  12718  strslfv  12723  setsslid  12729  strle1g  12784  1strbas  12795  2strbasg  12797  2stropg  12798  2strbas1g  12800  2strop1g  12801  rngbaseg  12813  rngplusgg  12814  rngmulrg  12815  srngbased  12824  srngplusgd  12825  srngmulrd  12826  srnginvld  12827  lmodbased  12842  lmodplusgd  12843  lmodscad  12844  lmodvscad  12845  ipsbased  12854  ipsaddgd  12855  ipsmulrd  12856  ipsscad  12857  ipsvscad  12858  ipsipd  12859  topgrpbasd  12874  topgrpplusgd  12875  topgrptsetd  12876  prdsex  12940  imasex  12948  imasival  12949  imasbas  12950  imasplusg  12951  imasmulr  12952  imasaddfnlemg  12957  imasaddvallemg  12958  xpsfval  12991  xpsval  12995  intopsn  13010  mgm1  13013  sgrp1  13054  mnd1  13087  mnd1id  13088  grp1  13238  grp1inv  13239  ring1  13615  psrval  14220  fnpsr  14221  psrbasg  14227  psrplusgg  14230  txlm  14515