Theorem opexg 4206

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 3756	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ = {{𝐴}, {𝐴, 𝐵}})
2		elex 2737	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
3		snexg 4163	. . . . 5 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
4	2, 3	syl 14	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
5	4	adantr 274	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴} ∈ V)
6		elex 2737	. . . 4 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
7		prexg 4189	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
8	2, 6, 7	syl2an 287	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
9		prexg 4189	. . 3 ⊢ (({𝐴} ∈ V ∧ {𝐴, 𝐵} ∈ V) → {{𝐴}, {𝐴, 𝐵}} ∈ V)
10	5, 8, 9	syl2anc 409	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {{𝐴}, {𝐴, 𝐵}} ∈ V)
11	1, 10	eqeltrd 2243	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ ∈ V)

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2136  Vcvv 2726  {csn 3576  {cpr 3577  ⟨cop 3579

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 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-14 2139  ax-ext 2147  ax-sep 4100  ax-pow 4153  ax-pr 4187

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-v 2728  df-un 3120  df-in 3122  df-ss 3129  df-pw 3561  df-sn 3582  df-pr 3583  df-op 3585

This theorem is referenced by:  opex  4207  otexg  4208  opeliunxp  4659  opbrop  4683  relsnopg  4708  opswapg  5090  elxp4  5091  elxp5  5092  resfunexg  5706  fliftel  5761  fliftel1  5762  oprabid  5874  ovexg  5876  eloprabga  5929  op1st  6114  op2nd  6115  ot1stg  6120  ot2ndg  6121  ot3rdgg  6122  elxp6  6137  mpofvex  6171  algrflem  6197  algrflemg  6198  mpoxopoveq  6208  brtposg  6222  tfr0dm  6290  tfrlemisucaccv  6293  tfrlemibxssdm  6295  tfrlemibfn  6296  tfrlemi14d  6301  tfr1onlemsucaccv  6309  tfr1onlembxssdm  6311  tfr1onlembfn  6312  tfr1onlemres  6317  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  tfrcllembfn  6325  tfrcllemres  6330  fnfi  6902  djulclb  7020  inl11  7030  1stinl  7039  2ndinl  7040  1stinr  7041  2ndinr  7042  mulpipq2  7312  enq0breq  7377  addvalex  7785  peano2nnnn  7794  axcnre  7822  frec2uzrdg  10344  frecuzrdg0  10348  frecuzrdgg  10351  frecuzrdg0t  10357  zfz1isolem1  10753  eucalgval2  11985  crth  12156  phimullem  12157  ennnfonelemp1  12339  setsvala  12425  setsex  12426  setsfun  12429  setsfun0  12430  setsresg  12432  setscom  12434  strslfv  12438  setsslid  12444  strle1g  12485  1strbas  12494  2strbasg  12496  2stropg  12497  2strbas1g  12499  2strop1g  12500  rngbaseg  12511  rngplusgg  12512  rngmulrg  12513  srngbased  12518  srngplusgd  12519  srngmulrd  12520  srnginvld  12521  lmodbased  12529  lmodplusgd  12530  lmodscad  12531  lmodvscad  12532  ipsbased  12537  ipsaddgd  12538  ipsmulrd  12539  ipsscad  12540  ipsvscad  12541  ipsipd  12542  topgrpbasd  12547  topgrpplusgd  12548  topgrptsetd  12549  intopsn  12598  mgm1  12601  txlm  12919