Theorem opexg 4315

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 3855	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ = {{𝐴}, {𝐴, 𝐵}})
2		elex 2811	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
3		snexg 4269	. . . . 5 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
4	2, 3	syl 14	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
5	4	adantr 276	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴} ∈ V)
6		elex 2811	. . . 4 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
7		prexg 4296	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
8	2, 6, 7	syl2an 289	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
9		prexg 4296	. . 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 2799  {csn 3666  {cpr 3667  ⟨cop 3669

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 4202  ax-pow 4259  ax-pr 4294

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 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675

This theorem is referenced by:  opex  4316  otexg  4317  opeliunxp  4776  opbrop  4800  relsnopg  4825  opswapg  5218  elxp4  5219  elxp5  5220  resfunexg  5867  fliftel  5926  fliftel1  5927  oprabid  6042  ovexg  6044  ovssunirng  6045  eloprabga  6100  op1st  6301  op2nd  6302  ot1stg  6307  ot2ndg  6308  ot3rdgg  6309  elxp6  6324  mpofvex  6362  algrflem  6386  algrflemg  6387  mpoxopoveq  6397  brtposg  6411  tfr0dm  6479  tfrlemisucaccv  6482  tfrlemibxssdm  6484  tfrlemibfn  6485  tfrlemi14d  6490  tfr1onlemsucaccv  6498  tfr1onlembxssdm  6500  tfr1onlembfn  6501  tfr1onlemres  6506  tfrcllemsucaccv  6511  tfrcllembxssdm  6513  tfrcllembfn  6514  tfrcllemres  6519  en2prd  6983  fnfi  7119  djulclb  7238  inl11  7248  1stinl  7257  2ndinl  7258  1stinr  7259  2ndinr  7260  mulpipq2  7574  enq0breq  7639  addvalex  8047  peano2nnnn  8056  axcnre  8084  frec2uzrdg  10648  frecuzrdg0  10652  frecuzrdgg  10655  frecuzrdg0t  10661  zfz1isolem1  11080  s1leng  11177  s111  11184  pfxclz  11232  eucalgval2  12596  crth  12767  phimullem  12768  ennnfonelemp1  12998  setsvala  13084  setsex  13085  setsfun  13088  setsfun0  13089  setsresg  13091  setscom  13093  strslfv  13098  strslfv3  13099  setsslid  13104  bassetsnn  13110  strle1g  13160  1strbas  13171  2strbasg  13174  2stropg  13175  2strbas1g  13177  2strop1g  13178  rngbaseg  13190  rngplusgg  13191  rngmulrg  13192  srngbased  13201  srngplusgd  13202  srngmulrd  13203  srnginvld  13204  lmodbased  13219  lmodplusgd  13220  lmodscad  13221  lmodvscad  13222  ipsbased  13231  ipsaddgd  13232  ipsmulrd  13233  ipsscad  13234  ipsvscad  13235  ipsipd  13236  topgrpbasd  13251  topgrpplusgd  13252  topgrptsetd  13253  prdsex  13323  prdsval  13327  imasex  13359  imasival  13360  imasbas  13361  imasplusg  13362  imasmulr  13363  imasaddfnlemg  13368  imasaddvallemg  13369  xpsfval  13402  xpsval  13406  intopsn  13421  mgm1  13424  sgrp1  13465  mnd1  13509  mnd1id  13510  grp1  13660  grp1inv  13661  ring1  14043  psrval  14651  fnpsr  14652  psrbasg  14659  psrplusgg  14663  txlm  14974  struct2slots2dom  15860  structvtxval  15861  structiedg0val  15862  structgrssvtx  15864  structgrssiedg  15865  gropd  15869  edgopval  15883  edgstruct  15885  isuhgropm  15902  uhgrunop  15908  upgrop  15925  upgr0eop  15943  upgr1eopdc  15944  upgrunop  15946  umgrunop  15948  isuspgropen  15983  isusgropen  15984  ausgrusgrben  15987  usgr0eop  16061  uspgr1eopdc  16062  usgr1eop  16064  vtxdgop  16078