Theorem opexg 4314

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 4268	. . . . 5 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
4	2, 3	syl 14	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
5	4	adantr 276	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴} ∈ V)
6		elex 2811	. . . 4 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
7		prexg 4295	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
8	2, 6, 7	syl2an 289	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
9		prexg 4295	. . 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 4258  ax-pr 4293

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  4315  otexg  4316  opeliunxp  4774  opbrop  4798  relsnopg  4823  opswapg  5215  elxp4  5216  elxp5  5217  resfunexg  5864  fliftel  5923  fliftel1  5924  oprabid  6039  ovexg  6041  ovssunirng  6042  eloprabga  6097  op1st  6298  op2nd  6299  ot1stg  6304  ot2ndg  6305  ot3rdgg  6306  elxp6  6321  mpofvex  6357  algrflem  6381  algrflemg  6382  mpoxopoveq  6392  brtposg  6406  tfr0dm  6474  tfrlemisucaccv  6477  tfrlemibxssdm  6479  tfrlemibfn  6480  tfrlemi14d  6485  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfr1onlemres  6501  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemres  6514  en2prd  6978  fnfi  7111  djulclb  7230  inl11  7240  1stinl  7249  2ndinl  7250  1stinr  7251  2ndinr  7252  mulpipq2  7566  enq0breq  7631  addvalex  8039  peano2nnnn  8048  axcnre  8076  frec2uzrdg  10639  frecuzrdg0  10643  frecuzrdgg  10646  frecuzrdg0t  10652  zfz1isolem1  11070  s1leng  11165  s111  11172  pfxclz  11219  eucalgval2  12583  crth  12754  phimullem  12755  ennnfonelemp1  12985  setsvala  13071  setsex  13072  setsfun  13075  setsfun0  13076  setsresg  13078  setscom  13080  strslfv  13085  strslfv3  13086  setsslid  13091  bassetsnn  13097  strle1g  13147  1strbas  13158  2strbasg  13161  2stropg  13162  2strbas1g  13164  2strop1g  13165  rngbaseg  13177  rngplusgg  13178  rngmulrg  13179  srngbased  13188  srngplusgd  13189  srngmulrd  13190  srnginvld  13191  lmodbased  13206  lmodplusgd  13207  lmodscad  13208  lmodvscad  13209  ipsbased  13218  ipsaddgd  13219  ipsmulrd  13220  ipsscad  13221  ipsvscad  13222  ipsipd  13223  topgrpbasd  13238  topgrpplusgd  13239  topgrptsetd  13240  prdsex  13310  prdsval  13314  imasex  13346  imasival  13347  imasbas  13348  imasplusg  13349  imasmulr  13350  imasaddfnlemg  13355  imasaddvallemg  13356  xpsfval  13389  xpsval  13393  intopsn  13408  mgm1  13411  sgrp1  13452  mnd1  13496  mnd1id  13497  grp1  13647  grp1inv  13648  ring1  14030  psrval  14638  fnpsr  14639  psrbasg  14646  psrplusgg  14650  txlm  14961  struct2slots2dom  15847  structvtxval  15848  structiedg0val  15849  structgrssvtx  15851  structgrssiedg  15852  gropd  15856  edgopval  15870  edgstruct  15872  isuhgropm  15889  uhgrunop  15895  upgrop  15912  upgr0eop  15930  upgr1eopdc  15931  upgrunop  15933  umgrunop  15935  isuspgropen  15970  isusgropen  15971  ausgrusgrben  15974