Theorem opexg 4150

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 3703	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ = {{𝐴}, {𝐴, 𝐵}})
2		elex 2697	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
3		snexg 4108	. . . . 5 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
4	2, 3	syl 14	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
5	4	adantr 274	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴} ∈ V)
6		elex 2697	. . . 4 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
7		prexg 4133	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
8	2, 6, 7	syl2an 287	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
9		prexg 4133	. . 3 ⊢ (({𝐴} ∈ V ∧ {𝐴, 𝐵} ∈ V) → {{𝐴}, {𝐴, 𝐵}} ∈ V)
10	5, 8, 9	syl2anc 408	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {{𝐴}, {𝐴, 𝐵}} ∈ V)
11	1, 10	eqeltrd 2216	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ ∈ V)

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1480  Vcvv 2686  {csn 3527  {cpr 3528  ⟨cop 3530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-pow 4098  ax-pr 4131

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536

This theorem is referenced by:  opex  4151  otexg  4152  opeliunxp  4594  opbrop  4618  relsnopg  4643  opswapg  5025  elxp4  5026  elxp5  5027  resfunexg  5641  fliftel  5694  fliftel1  5695  oprabid  5803  ovexg  5805  eloprabga  5858  op1st  6044  op2nd  6045  ot1stg  6050  ot2ndg  6051  ot3rdgg  6052  elxp6  6067  mpofvex  6101  algrflem  6126  algrflemg  6127  mpoxopoveq  6137  brtposg  6151  tfr0dm  6219  tfrlemisucaccv  6222  tfrlemibxssdm  6224  tfrlemibfn  6225  tfrlemi14d  6230  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfr1onlemres  6246  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemres  6259  fnfi  6825  djulclb  6940  inl11  6950  1stinl  6959  2ndinl  6960  1stinr  6961  2ndinr  6962  mulpipq2  7179  enq0breq  7244  addvalex  7652  peano2nnnn  7661  axcnre  7689  frec2uzrdg  10182  frecuzrdg0  10186  frecuzrdgg  10189  frecuzrdg0t  10195  zfz1isolem1  10583  eucalgval2  11734  crth  11900  phimullem  11901  ennnfonelemp1  11919  setsvala  11990  setsex  11991  setsfun  11994  setsfun0  11995  setsresg  11997  setscom  11999  strslfv  12003  setsslid  12009  strle1g  12049  1strbas  12058  2strbasg  12060  2stropg  12061  2strbas1g  12063  2strop1g  12064  rngbaseg  12075  rngplusgg  12076  rngmulrg  12077  srngbased  12082  srngplusgd  12083  srngmulrd  12084  srnginvld  12085  lmodbased  12093  lmodplusgd  12094  lmodscad  12095  lmodvscad  12096  ipsbased  12101  ipsaddgd  12102  ipsmulrd  12103  ipsscad  12104  ipsvscad  12105  ipsipd  12106  topgrpbasd  12111  topgrpplusgd  12112  topgrptsetd  12113  txlm  12448