Theorem opexg 4326

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  Vcvv 2803  {csn 3673  {cpr 3674  ⟨cop 3676

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 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682

This theorem is referenced by:  opex  4327  otexg  4328  opeliunxp  4787  opbrop  4811  relsnopg  4836  opswapg  5230  elxp4  5231  elxp5  5232  resfunexg  5883  fliftel  5944  fliftel1  5945  oprabid  6060  ovexg  6062  ovssunirng  6063  eloprabga  6118  op1st  6318  op2nd  6319  ot1stg  6324  ot2ndg  6325  ot3rdgg  6326  elxp6  6341  mpofvex  6379  algrflem  6403  algrflemg  6404  mpoxopoveq  6449  brtposg  6463  tfr0dm  6531  tfrlemisucaccv  6534  tfrlemibxssdm  6536  tfrlemibfn  6537  tfrlemi14d  6542  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemres  6558  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemres  6571  en2prd  7035  fnfi  7178  djulclb  7297  inl11  7307  1stinl  7316  2ndinl  7317  1stinr  7318  2ndinr  7319  mulpipq2  7634  enq0breq  7699  addvalex  8107  peano2nnnn  8116  axcnre  8144  frec2uzrdg  10715  frecuzrdg0  10719  frecuzrdgg  10722  frecuzrdg0t  10728  zfz1isolem1  11148  s1leng  11248  s111  11255  pfxclz  11307  eucalgval2  12686  crth  12857  phimullem  12858  ennnfonelemp1  13088  setsvala  13174  setsex  13175  setsfun  13178  setsfun0  13179  setsresg  13181  setscom  13183  strslfv  13188  strslfv3  13189  setsslid  13194  bassetsnn  13200  strle1g  13250  1strbas  13261  2strbasg  13264  2stropg  13265  2strbas1g  13267  2strop1g  13268  rngbaseg  13280  rngplusgg  13281  rngmulrg  13282  srngbased  13291  srngplusgd  13292  srngmulrd  13293  srnginvld  13294  lmodbased  13309  lmodplusgd  13310  lmodscad  13311  lmodvscad  13312  ipsbased  13321  ipsaddgd  13322  ipsmulrd  13323  ipsscad  13324  ipsvscad  13325  ipsipd  13326  topgrpbasd  13341  topgrpplusgd  13342  topgrptsetd  13343  prdsex  13413  prdsval  13417  imasex  13449  imasival  13450  imasbas  13451  imasplusg  13452  imasmulr  13453  imasaddfnlemg  13458  imasaddvallemg  13459  xpsfval  13492  xpsval  13496  intopsn  13511  mgm1  13514  sgrp1  13555  mnd1  13599  mnd1id  13600  grp1  13750  grp1inv  13751  ring1  14134  psrval  14742  fnpsr  14743  psrbasg  14755  psrplusgg  14759  txlm  15070  struct2slots2dom  15959  structvtxval  15960  structiedg0val  15961  structgrssvtx  15963  structgrssiedg  15964  gropd  15968  edgopval  15983  edgstruct  15985  isuhgropm  16002  uhgrunop  16008  upgrop  16025  upgr0eop  16043  upgr1eopdc  16044  upgr1een  16045  umgr1een  16046  upgrunop  16048  umgrunop  16050  isuspgropen  16085  isusgropen  16086  ausgrusgrben  16089  usgr0eop  16163  uspgr1eopdc  16164  usgr1eop  16166  uhgrspanop  16203  vtxdgop  16213  p1evtxdeqfilem  16232  p1evtxdeqfi  16233  p1evtxdp1fi  16234  eupthvdres  16396  eupth2lem3fi  16397  konigsbergumgr  16408