Theorem opexg 4343

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2203  Vcvv 2812  {csn 3688  {cpr 3689  ⟨cop 3691

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 2206  ax-ext 2214  ax-sep 4227  ax-pow 4286  ax-pr 4321

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814  df-un 3214  df-in 3216  df-ss 3223  df-pw 3670  df-sn 3694  df-pr 3695  df-op 3697

This theorem is referenced by:  opex  4344  otexg  4345  opeliunxp  4804  opbrop  4828  relsnopg  4853  opswapg  5248  elxp4  5249  elxp5  5250  resfunexg  5904  fliftel  5965  fliftel1  5966  oprabid  6081  ovexg  6083  ovssunirng  6084  eloprabga  6139  op1st  6339  op2nd  6340  ot1stg  6345  ot2ndg  6346  ot3rdgg  6347  elxp6  6362  mpofvex  6400  algrflem  6424  algrflemg  6425  mpoxopoveq  6470  brtposg  6484  tfr0dm  6552  tfrlemisucaccv  6555  tfrlemibxssdm  6557  tfrlemibfn  6558  tfrlemi14d  6563  tfr1onlemsucaccv  6571  tfr1onlembxssdm  6573  tfr1onlembfn  6574  tfr1onlemres  6579  tfrcllemsucaccv  6584  tfrcllembxssdm  6586  tfrcllembfn  6587  tfrcllemres  6592  mapsnend  7051  en2prd  7058  fnfi  7202  snopfsuppdc  7251  djulclb  7345  inl11  7355  1stinl  7364  2ndinl  7365  1stinr  7366  2ndinr  7367  mulpipq2  7685  enq0breq  7750  addvalex  8158  peano2nnnn  8167  axcnre  8195  frec2uzrdg  10770  frecuzrdg0  10774  frecuzrdgg  10777  frecuzrdg0t  10783  zfz1isolem1  11208  s1leng  11308  s111  11315  pfxclz  11367  eucalgval2  12746  crth  12917  phimullem  12918  ennnfonelemp1  13149  setsvala  13235  setsex  13236  setsfun  13239  setsfun0  13240  setsresg  13242  setscom  13244  strslfv  13249  strslfv3  13250  setsslid  13255  bassetsnn  13261  strle1g  13311  1strbas  13322  2strbasg  13325  2stropg  13326  2strbas1g  13328  2strop1g  13329  rngbaseg  13341  rngplusgg  13342  rngmulrg  13343  srngbased  13352  srngplusgd  13353  srngmulrd  13354  srnginvld  13355  lmodbased  13370  lmodplusgd  13371  lmodscad  13372  lmodvscad  13373  ipsbased  13382  ipsaddgd  13383  ipsmulrd  13384  ipsscad  13385  ipsvscad  13386  ipsipd  13387  topgrpbasd  13402  topgrpplusgd  13403  topgrptsetd  13404  prdsex  13474  prdsval  13478  imasex  13510  imasival  13511  imasbas  13512  imasplusg  13513  imasmulr  13514  imasaddfnlemg  13519  imasaddvallemg  13520  xpsfval  13553  xpsval  13557  intopsn  13572  mgm1  13575  sgrp1  13616  mnd1  13660  mnd1id  13661  grp1  13811  grp1inv  13812  ring1  14195  psrval  14806  fnpsr  14807  psrbasg  14821  psrplusgg  14825  txlm  15136  struct2slots2dom  16025  structvtxval  16026  structiedg0val  16027  structgrssvtx  16029  structgrssiedg  16030  gropd  16034  edgopval  16049  edgstruct  16051  isuhgropm  16068  uhgrunop  16074  upgrop  16091  upgr0eop  16109  upgr1eopdc  16110  upgr1een  16111  umgr1een  16112  upgrunop  16114  umgrunop  16116  isuspgropen  16151  isusgropen  16152  ausgrusgrben  16155  usgr0eop  16229  uspgr1eopdc  16230  usgr1eop  16232  uhgrspanop  16269  vtxdgop  16279  p1evtxdeqfilem  16298  p1evtxdeqfi  16299  p1evtxdp1fi  16300  eupthvdres  16462  eupth2lem3fi  16463  konigsbergumgr  16474