Theorem opexg 4366

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 3900	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ = {{𝐴}, {𝐴, 𝐵}})
2		elex 2833	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
3		snexg 4319	. . . . 5 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
4	2, 3	syl 14	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
5	4	adantr 276	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴} ∈ V)
6		elex 2833	. . . 4 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
7		prexg 4347	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
8	2, 6, 7	syl2an 289	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
9		prexg 4347	. . 3 ⊢ (({𝐴} ∈ V ∧ {𝐴, 𝐵} ∈ V) → {{𝐴}, {𝐴, 𝐵}} ∈ V)
10	5, 8, 9	syl2anc 415	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {{𝐴}, {𝐴, 𝐵}} ∈ V)
11	1, 10	eqeltrd 2315	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ ∈ V)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2209  Vcvv 2821  {csn 3708  {cpr 3709  ⟨cop 3711

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4247  ax-pow 4309  ax-pr 4344

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3714  df-pr 3715  df-op 3717

This theorem is referenced by:  opex  4367  otexg  4368  opeliunxp  4828  opbrop  4852  relsnopg  4877  opswapg  5272  elxp4  5273  elxp5  5274  resfunexg  5930  fliftel  5993  fliftel1  5994  oprabid  6111  ovexg  6113  ovssunirng  6114  eloprabga  6169  op1st  6374  op2nd  6375  ot1stg  6380  ot2ndg  6381  ot3rdgg  6382  elxp6  6397  mpofvex  6435  algrflem  6459  algrflemg  6460  mpoxopoveq  6505  brtposg  6519  tfr0dm  6587  tfrlemisucaccv  6590  tfrlemibxssdm  6592  tfrlemibfn  6593  tfrlemi14d  6598  tfr1onlemsucaccv  6606  tfr1onlembxssdm  6608  tfr1onlembfn  6609  tfr1onlemres  6614  tfrcllemsucaccv  6619  tfrcllembxssdm  6621  tfrcllembfn  6622  tfrcllemres  6627  mapsnend  7093  en2prd  7100  fnfi  7244  snopfsuppdc  7293  djulclb  7389  inl11  7399  1stinl  7408  2ndinl  7409  1stinr  7410  2ndinr  7411  mulpipq2  7732  enq0breq  7797  addvalex  8205  peano2nnnn  8214  axcnre  8242  frec2uzrdg  10829  frecuzrdg0  10833  frecuzrdgg  10836  frecuzrdg0t  10842  zfz1isolem1  11275  s1leng  11375  s111  11382  pfxclz  11434  eucalgval2  12814  crth  12985  phimullem  12986  ennnfonelemp1  13280  setsvala  13366  setsex  13367  setsfun  13370  setsfun0  13371  setsresg  13373  setscom  13375  strslfv  13380  strslfv3  13381  setsslid  13386  bassetsnn  13392  strle1g  13443  1strbas  13454  2strbasg  13457  2stropg  13458  2strbas1g  13460  2strop1g  13461  rngbaseg  13473  rngplusgg  13474  rngmulrg  13475  srngbased  13484  srngplusgd  13485  srngmulrd  13486  srnginvld  13487  lmodbased  13502  lmodplusgd  13503  lmodscad  13504  lmodvscad  13505  ipsbased  13514  ipsaddgd  13515  ipsmulrd  13516  ipsscad  13517  ipsvscad  13518  ipsipd  13519  topgrpbasd  13534  topgrpplusgd  13535  topgrptsetd  13536  imasex  13609  imasival  13610  imasbas  13611  imasplusg  13612  imasmulr  13613  imasaddfnlemg  13618  imasaddvallemg  13619  xpsfval  13652  intopsn  13670  mgm1  13673  sgrp1  13709  mnd1  13745  mnd1id  13746  grp1  13894  grp1inv  13895  prdsex  14155  prdsval  14156  xpsval  14184  ring1  14347  psrval  15033  fnpsr  15034  psrbasg  15048  psrplusgg  15052  txlm  15363  struct2slots2dom  16262  structvtxval  16263  structiedg0val  16264  structgrssvtx  16266  structgrssiedg  16267  gropd  16271  edgopval  16286  edgstruct  16288  isuhgropm  16305  uhgrunop  16311  upgrop  16328  upgr0eop  16346  upgr1eopdc  16347  upgr1een  16348  umgr1een  16349  upgrunop  16351  umgrunop  16353  isuspgropen  16388  isusgropen  16389  ausgrusgrben  16392  usgr0eop  16466  uspgr1eopdc  16467  usgr1eop  16469  uhgrspanop  16506  vtxdgop  16516  p1evtxdeqfilem  16535  p1evtxdeqfi  16536  p1evtxdp1fi  16537  eupthvdres  16699  eupth2lem3fi  16700  konigsbergumgr  16711