Theorem opexg 4258

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2164  Vcvv 2760  {csn 3619  {cpr 3620  ⟨cop 3622

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2167  ax-ext 2175  ax-sep 4148  ax-pow 4204  ax-pr 4239

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-in 3160  df-ss 3167  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628

This theorem is referenced by:  opex  4259  otexg  4260  opeliunxp  4715  opbrop  4739  relsnopg  4764  opswapg  5153  elxp4  5154  elxp5  5155  resfunexg  5780  fliftel  5837  fliftel1  5838  oprabid  5951  ovexg  5953  eloprabga  6006  op1st  6201  op2nd  6202  ot1stg  6207  ot2ndg  6208  ot3rdgg  6209  elxp6  6224  mpofvex  6260  algrflem  6284  algrflemg  6285  mpoxopoveq  6295  brtposg  6309  tfr0dm  6377  tfrlemisucaccv  6380  tfrlemibxssdm  6382  tfrlemibfn  6383  tfrlemi14d  6388  tfr1onlemsucaccv  6396  tfr1onlembxssdm  6398  tfr1onlembfn  6399  tfr1onlemres  6404  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllembfn  6412  tfrcllemres  6417  fnfi  6997  djulclb  7116  inl11  7126  1stinl  7135  2ndinl  7136  1stinr  7137  2ndinr  7138  mulpipq2  7433  enq0breq  7498  addvalex  7906  peano2nnnn  7915  axcnre  7943  frec2uzrdg  10483  frecuzrdg0  10487  frecuzrdgg  10490  frecuzrdg0t  10496  zfz1isolem1  10914  eucalgval2  12194  crth  12365  phimullem  12366  ennnfonelemp1  12566  setsvala  12652  setsex  12653  setsfun  12656  setsfun0  12657  setsresg  12659  setscom  12661  strslfv  12666  setsslid  12672  strle1g  12727  1strbas  12738  2strbasg  12740  2stropg  12741  2strbas1g  12743  2strop1g  12744  rngbaseg  12756  rngplusgg  12757  rngmulrg  12758  srngbased  12767  srngplusgd  12768  srngmulrd  12769  srnginvld  12770  lmodbased  12785  lmodplusgd  12786  lmodscad  12787  lmodvscad  12788  ipsbased  12797  ipsaddgd  12798  ipsmulrd  12799  ipsscad  12800  ipsvscad  12801  ipsipd  12802  topgrpbasd  12817  topgrpplusgd  12818  topgrptsetd  12819  prdsex  12883  imasex  12891  imasival  12892  imasbas  12893  imasplusg  12894  imasmulr  12895  imasaddfnlemg  12900  imasaddvallemg  12901  xpsfval  12934  xpsval  12938  intopsn  12953  mgm1  12956  sgrp1  12997  mnd1  13030  mnd1id  13031  grp1  13181  grp1inv  13182  ring1  13558  psrval  14163  fnpsr  14164  psrbasg  14170  psrplusgg  14173  txlm  14458