Theorem opexg 4320

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  Vcvv 2802  {csn 3669  {cpr 3670  ⟨cop 3672

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678

This theorem is referenced by:  opex  4321  otexg  4322  opeliunxp  4781  opbrop  4805  relsnopg  4830  opswapg  5223  elxp4  5224  elxp5  5225  resfunexg  5875  fliftel  5934  fliftel1  5935  oprabid  6050  ovexg  6052  ovssunirng  6053  eloprabga  6108  op1st  6309  op2nd  6310  ot1stg  6315  ot2ndg  6316  ot3rdgg  6317  elxp6  6332  mpofvex  6370  algrflem  6394  algrflemg  6395  mpoxopoveq  6406  brtposg  6420  tfr0dm  6488  tfrlemisucaccv  6491  tfrlemibxssdm  6493  tfrlemibfn  6494  tfrlemi14d  6499  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemres  6515  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemres  6528  en2prd  6992  fnfi  7135  djulclb  7254  inl11  7264  1stinl  7273  2ndinl  7274  1stinr  7275  2ndinr  7276  mulpipq2  7591  enq0breq  7656  addvalex  8064  peano2nnnn  8073  axcnre  8101  frec2uzrdg  10672  frecuzrdg0  10676  frecuzrdgg  10679  frecuzrdg0t  10685  zfz1isolem1  11105  s1leng  11205  s111  11212  pfxclz  11264  eucalgval2  12630  crth  12801  phimullem  12802  ennnfonelemp1  13032  setsvala  13118  setsex  13119  setsfun  13122  setsfun0  13123  setsresg  13125  setscom  13127  strslfv  13132  strslfv3  13133  setsslid  13138  bassetsnn  13144  strle1g  13194  1strbas  13205  2strbasg  13208  2stropg  13209  2strbas1g  13211  2strop1g  13212  rngbaseg  13224  rngplusgg  13225  rngmulrg  13226  srngbased  13235  srngplusgd  13236  srngmulrd  13237  srnginvld  13238  lmodbased  13253  lmodplusgd  13254  lmodscad  13255  lmodvscad  13256  ipsbased  13265  ipsaddgd  13266  ipsmulrd  13267  ipsscad  13268  ipsvscad  13269  ipsipd  13270  topgrpbasd  13285  topgrpplusgd  13286  topgrptsetd  13287  prdsex  13357  prdsval  13361  imasex  13393  imasival  13394  imasbas  13395  imasplusg  13396  imasmulr  13397  imasaddfnlemg  13402  imasaddvallemg  13403  xpsfval  13436  xpsval  13440  intopsn  13455  mgm1  13458  sgrp1  13499  mnd1  13543  mnd1id  13544  grp1  13694  grp1inv  13695  ring1  14078  psrval  14686  fnpsr  14687  psrbasg  14694  psrplusgg  14698  txlm  15009  struct2slots2dom  15895  structvtxval  15896  structiedg0val  15897  structgrssvtx  15899  structgrssiedg  15900  gropd  15904  edgopval  15919  edgstruct  15921  isuhgropm  15938  uhgrunop  15944  upgrop  15961  upgr0eop  15979  upgr1eopdc  15980  upgr1een  15981  umgr1een  15982  upgrunop  15984  umgrunop  15986  isuspgropen  16021  isusgropen  16022  ausgrusgrben  16025  usgr0eop  16099  uspgr1eopdc  16100  usgr1eop  16102  uhgrspanop  16139  vtxdgop  16149  p1evtxdeqfilem  16168  p1evtxdeqfi  16169  p1evtxdp1fi  16170  eupthvdres  16332  eupth2lem3fi  16333