Theorem opexg 4229

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  Vcvv 2738  {csn 3593  {cpr 3594  ⟨cop 3596

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602

This theorem is referenced by:  opex  4230  otexg  4231  opeliunxp  4682  opbrop  4706  relsnopg  4731  opswapg  5116  elxp4  5117  elxp5  5118  resfunexg  5738  fliftel  5794  fliftel1  5795  oprabid  5907  ovexg  5909  eloprabga  5962  op1st  6147  op2nd  6148  ot1stg  6153  ot2ndg  6154  ot3rdgg  6155  elxp6  6170  mpofvex  6204  algrflem  6230  algrflemg  6231  mpoxopoveq  6241  brtposg  6255  tfr0dm  6323  tfrlemisucaccv  6326  tfrlemibxssdm  6328  tfrlemibfn  6329  tfrlemi14d  6334  tfr1onlemsucaccv  6342  tfr1onlembxssdm  6344  tfr1onlembfn  6345  tfr1onlemres  6350  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllembfn  6358  tfrcllemres  6363  fnfi  6936  djulclb  7054  inl11  7064  1stinl  7073  2ndinl  7074  1stinr  7075  2ndinr  7076  mulpipq2  7370  enq0breq  7435  addvalex  7843  peano2nnnn  7852  axcnre  7880  frec2uzrdg  10409  frecuzrdg0  10413  frecuzrdgg  10416  frecuzrdg0t  10422  zfz1isolem1  10820  eucalgval2  12053  crth  12224  phimullem  12225  ennnfonelemp1  12407  setsvala  12493  setsex  12494  setsfun  12497  setsfun0  12498  setsresg  12500  setscom  12502  strslfv  12507  setsslid  12513  strle1g  12565  1strbas  12576  2strbasg  12578  2stropg  12579  2strbas1g  12581  2strop1g  12582  rngbaseg  12594  rngplusgg  12595  rngmulrg  12596  srngbased  12605  srngplusgd  12606  srngmulrd  12607  srnginvld  12608  lmodbased  12623  lmodplusgd  12624  lmodscad  12625  lmodvscad  12626  ipsbased  12635  ipsaddgd  12636  ipsmulrd  12637  ipsscad  12638  ipsvscad  12639  ipsipd  12640  topgrpbasd  12652  topgrpplusgd  12653  topgrptsetd  12654  prdsex  12718  imasex  12726  imasival  12727  imasbas  12728  imasplusg  12729  imasmulr  12730  imasaddfnlemg  12735  imasaddvallemg  12736  xpsfval  12767  xpsval  12771  intopsn  12786  mgm1  12789  sgrp1  12816  mnd1  12847  mnd1id  12848  grp1  12976  grp1inv  12977  ring1  13236  txlm  13782