Theorem opexg 4318

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  Vcvv 2800  {csn 3667  {cpr 3668  ⟨cop 3670

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-pow 4262  ax-pr 4297

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676

This theorem is referenced by:  opex  4319  otexg  4320  opeliunxp  4779  opbrop  4803  relsnopg  4828  opswapg  5221  elxp4  5222  elxp5  5223  resfunexg  5870  fliftel  5929  fliftel1  5930  oprabid  6045  ovexg  6047  ovssunirng  6048  eloprabga  6103  op1st  6304  op2nd  6305  ot1stg  6310  ot2ndg  6311  ot3rdgg  6312  elxp6  6327  mpofvex  6365  algrflem  6389  algrflemg  6390  mpoxopoveq  6401  brtposg  6415  tfr0dm  6483  tfrlemisucaccv  6486  tfrlemibxssdm  6488  tfrlemibfn  6489  tfrlemi14d  6494  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfr1onlemres  6510  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllembfn  6518  tfrcllemres  6523  en2prd  6987  fnfi  7129  djulclb  7248  inl11  7258  1stinl  7267  2ndinl  7268  1stinr  7269  2ndinr  7270  mulpipq2  7584  enq0breq  7649  addvalex  8057  peano2nnnn  8066  axcnre  8094  frec2uzrdg  10664  frecuzrdg0  10668  frecuzrdgg  10671  frecuzrdg0t  10677  zfz1isolem1  11097  s1leng  11194  s111  11201  pfxclz  11253  eucalgval2  12618  crth  12789  phimullem  12790  ennnfonelemp1  13020  setsvala  13106  setsex  13107  setsfun  13110  setsfun0  13111  setsresg  13113  setscom  13115  strslfv  13120  strslfv3  13121  setsslid  13126  bassetsnn  13132  strle1g  13182  1strbas  13193  2strbasg  13196  2stropg  13197  2strbas1g  13199  2strop1g  13200  rngbaseg  13212  rngplusgg  13213  rngmulrg  13214  srngbased  13223  srngplusgd  13224  srngmulrd  13225  srnginvld  13226  lmodbased  13241  lmodplusgd  13242  lmodscad  13243  lmodvscad  13244  ipsbased  13253  ipsaddgd  13254  ipsmulrd  13255  ipsscad  13256  ipsvscad  13257  ipsipd  13258  topgrpbasd  13273  topgrpplusgd  13274  topgrptsetd  13275  prdsex  13345  prdsval  13349  imasex  13381  imasival  13382  imasbas  13383  imasplusg  13384  imasmulr  13385  imasaddfnlemg  13390  imasaddvallemg  13391  xpsfval  13424  xpsval  13428  intopsn  13443  mgm1  13446  sgrp1  13487  mnd1  13531  mnd1id  13532  grp1  13682  grp1inv  13683  ring1  14065  psrval  14673  fnpsr  14674  psrbasg  14681  psrplusgg  14685  txlm  14996  struct2slots2dom  15882  structvtxval  15883  structiedg0val  15884  structgrssvtx  15886  structgrssiedg  15887  gropd  15891  edgopval  15906  edgstruct  15908  isuhgropm  15925  uhgrunop  15931  upgrop  15948  upgr0eop  15966  upgr1eopdc  15967  upgr1een  15968  umgr1een  15969  upgrunop  15971  umgrunop  15973  isuspgropen  16008  isusgropen  16009  ausgrusgrben  16012  usgr0eop  16086  uspgr1eopdc  16087  usgr1eop  16089  vtxdgop  16103  p1evtxdeqfilem  16122  p1evtxdeqfi  16123  p1evtxdp1fi  16124