Theorem opexg 4349

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  Vcvv 2815  {csn 3694  {cpr 3695  ⟨cop 3697

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703

This theorem is referenced by:  opex  4350  otexg  4351  opeliunxp  4810  opbrop  4834  relsnopg  4859  opswapg  5254  elxp4  5255  elxp5  5256  resfunexg  5910  fliftel  5972  fliftel1  5973  oprabid  6090  ovexg  6092  ovssunirng  6093  eloprabga  6148  op1st  6353  op2nd  6354  ot1stg  6359  ot2ndg  6360  ot3rdgg  6361  elxp6  6376  mpofvex  6414  algrflem  6438  algrflemg  6439  mpoxopoveq  6484  brtposg  6498  tfr0dm  6566  tfrlemisucaccv  6569  tfrlemibxssdm  6571  tfrlemibfn  6572  tfrlemi14d  6577  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfr1onlemres  6593  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllembfn  6601  tfrcllemres  6606  mapsnend  7065  en2prd  7072  fnfi  7216  snopfsuppdc  7265  djulclb  7359  inl11  7369  1stinl  7378  2ndinl  7379  1stinr  7380  2ndinr  7381  mulpipq2  7702  enq0breq  7767  addvalex  8175  peano2nnnn  8184  axcnre  8212  frec2uzrdg  10795  frecuzrdg0  10799  frecuzrdgg  10802  frecuzrdg0t  10808  zfz1isolem1  11237  s1leng  11337  s111  11344  pfxclz  11396  eucalgval2  12775  crth  12946  phimullem  12947  ennnfonelemp1  13241  setsvala  13327  setsex  13328  setsfun  13331  setsfun0  13332  setsresg  13334  setscom  13336  strslfv  13341  strslfv3  13342  setsslid  13347  bassetsnn  13353  strle1g  13403  1strbas  13414  2strbasg  13417  2stropg  13418  2strbas1g  13420  2strop1g  13421  rngbaseg  13433  rngplusgg  13434  rngmulrg  13435  srngbased  13444  srngplusgd  13445  srngmulrd  13446  srnginvld  13447  lmodbased  13462  lmodplusgd  13463  lmodscad  13464  lmodvscad  13465  ipsbased  13474  ipsaddgd  13475  ipsmulrd  13476  ipsscad  13477  ipsvscad  13478  ipsipd  13479  topgrpbasd  13494  topgrpplusgd  13495  topgrptsetd  13496  prdsex  13566  prdsval  13570  imasex  13602  imasival  13603  imasbas  13604  imasplusg  13605  imasmulr  13606  imasaddfnlemg  13611  imasaddvallemg  13612  xpsfval  13645  xpsval  13649  intopsn  13664  mgm1  13667  sgrp1  13708  mnd1  13752  mnd1id  13753  grp1  13903  grp1inv  13904  ring1  14287  psrval  14926  fnpsr  14927  psrbasg  14941  psrplusgg  14945  txlm  15256  struct2slots2dom  16145  structvtxval  16146  structiedg0val  16147  structgrssvtx  16149  structgrssiedg  16150  gropd  16154  edgopval  16169  edgstruct  16171  isuhgropm  16188  uhgrunop  16194  upgrop  16211  upgr0eop  16229  upgr1eopdc  16230  upgr1een  16231  umgr1een  16232  upgrunop  16234  umgrunop  16236  isuspgropen  16271  isusgropen  16272  ausgrusgrben  16275  usgr0eop  16349  uspgr1eopdc  16350  usgr1eop  16352  uhgrspanop  16389  vtxdgop  16399  p1evtxdeqfilem  16418  p1evtxdeqfi  16419  p1evtxdp1fi  16420  eupthvdres  16582  eupth2lem3fi  16583  konigsbergumgr  16594