Theorem opexg 4313

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 3854	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ = {{𝐴}, {𝐴, 𝐵}})
2		elex 2811	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
3		snexg 4267	. . . . 5 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
4	2, 3	syl 14	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
5	4	adantr 276	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴} ∈ V)
6		elex 2811	. . . 4 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
7		prexg 4294	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
8	2, 6, 7	syl2an 289	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
9		prexg 4294	. . 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 4201  ax-pow 4257  ax-pr 4292

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  4314  otexg  4315  opeliunxp  4771  opbrop  4795  relsnopg  4820  opswapg  5211  elxp4  5212  elxp5  5213  resfunexg  5853  fliftel  5910  fliftel1  5911  oprabid  6026  ovexg  6028  ovssunirng  6029  eloprabga  6082  op1st  6282  op2nd  6283  ot1stg  6288  ot2ndg  6289  ot3rdgg  6290  elxp6  6305  mpofvex  6341  algrflem  6365  algrflemg  6366  mpoxopoveq  6376  brtposg  6390  tfr0dm  6458  tfrlemisucaccv  6461  tfrlemibxssdm  6463  tfrlemibfn  6464  tfrlemi14d  6469  tfr1onlemsucaccv  6477  tfr1onlembxssdm  6479  tfr1onlembfn  6480  tfr1onlemres  6485  tfrcllemsucaccv  6490  tfrcllembxssdm  6492  tfrcllembfn  6493  tfrcllemres  6498  en2prd  6960  fnfi  7091  djulclb  7210  inl11  7220  1stinl  7229  2ndinl  7230  1stinr  7231  2ndinr  7232  mulpipq2  7546  enq0breq  7611  addvalex  8019  peano2nnnn  8028  axcnre  8056  frec2uzrdg  10618  frecuzrdg0  10622  frecuzrdgg  10625  frecuzrdg0t  10631  zfz1isolem1  11049  s1leng  11143  s111  11150  pfxclz  11197  eucalgval2  12561  crth  12732  phimullem  12733  ennnfonelemp1  12963  setsvala  13049  setsex  13050  setsfun  13053  setsfun0  13054  setsresg  13056  setscom  13058  strslfv  13063  strslfv3  13064  setsslid  13069  bassetsnn  13075  strle1g  13125  1strbas  13136  2strbasg  13139  2stropg  13140  2strbas1g  13142  2strop1g  13143  rngbaseg  13155  rngplusgg  13156  rngmulrg  13157  srngbased  13166  srngplusgd  13167  srngmulrd  13168  srnginvld  13169  lmodbased  13184  lmodplusgd  13185  lmodscad  13186  lmodvscad  13187  ipsbased  13196  ipsaddgd  13197  ipsmulrd  13198  ipsscad  13199  ipsvscad  13200  ipsipd  13201  topgrpbasd  13216  topgrpplusgd  13217  topgrptsetd  13218  prdsex  13288  prdsval  13292  imasex  13324  imasival  13325  imasbas  13326  imasplusg  13327  imasmulr  13328  imasaddfnlemg  13333  imasaddvallemg  13334  xpsfval  13367  xpsval  13371  intopsn  13386  mgm1  13389  sgrp1  13430  mnd1  13474  mnd1id  13475  grp1  13625  grp1inv  13626  ring1  14008  psrval  14615  fnpsr  14616  psrbasg  14623  psrplusgg  14627  txlm  14938  struct2slots2dom  15824  structvtxval  15825  structiedg0val  15826  structgrssvtx  15828  structgrssiedg  15829  gropd  15833  edgopval  15847  edgstruct  15849  isuhgropm  15866  uhgrunop  15872  upgrop  15889  upgr0eop  15907  upgr1eopdc  15908  upgrunop  15910  umgrunop  15912  isuspgropen  15947  isusgropen  15948  ausgrusgrben  15951