Theorem opexg 4230

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 3778	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ = {{𝐴}, {𝐴, 𝐵}})
2		elex 2750	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
3		snexg 4186	. . . . 5 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
4	2, 3	syl 14	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
5	4	adantr 276	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴} ∈ V)
6		elex 2750	. . . 4 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
7		prexg 4213	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
8	2, 6, 7	syl2an 289	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
9		prexg 4213	. . 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 2739  {csn 3594  {cpr 3595  ⟨cop 3597

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 4123  ax-pow 4176  ax-pr 4211

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 2741  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603

This theorem is referenced by:  opex  4231  otexg  4232  opeliunxp  4683  opbrop  4707  relsnopg  4732  opswapg  5117  elxp4  5118  elxp5  5119  resfunexg  5739  fliftel  5796  fliftel1  5797  oprabid  5909  ovexg  5911  eloprabga  5964  op1st  6149  op2nd  6150  ot1stg  6155  ot2ndg  6156  ot3rdgg  6157  elxp6  6172  mpofvex  6206  algrflem  6232  algrflemg  6233  mpoxopoveq  6243  brtposg  6257  tfr0dm  6325  tfrlemisucaccv  6328  tfrlemibxssdm  6330  tfrlemibfn  6331  tfrlemi14d  6336  tfr1onlemsucaccv  6344  tfr1onlembxssdm  6346  tfr1onlembfn  6347  tfr1onlemres  6352  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllembfn  6360  tfrcllemres  6365  fnfi  6938  djulclb  7056  inl11  7066  1stinl  7075  2ndinl  7076  1stinr  7077  2ndinr  7078  mulpipq2  7372  enq0breq  7437  addvalex  7845  peano2nnnn  7854  axcnre  7882  frec2uzrdg  10411  frecuzrdg0  10415  frecuzrdgg  10418  frecuzrdg0t  10424  zfz1isolem1  10822  eucalgval2  12055  crth  12226  phimullem  12227  ennnfonelemp1  12409  setsvala  12495  setsex  12496  setsfun  12499  setsfun0  12500  setsresg  12502  setscom  12504  strslfv  12509  setsslid  12515  strle1g  12567  1strbas  12578  2strbasg  12580  2stropg  12581  2strbas1g  12583  2strop1g  12584  rngbaseg  12596  rngplusgg  12597  rngmulrg  12598  srngbased  12607  srngplusgd  12608  srngmulrd  12609  srnginvld  12610  lmodbased  12625  lmodplusgd  12626  lmodscad  12627  lmodvscad  12628  ipsbased  12637  ipsaddgd  12638  ipsmulrd  12639  ipsscad  12640  ipsvscad  12641  ipsipd  12642  topgrpbasd  12657  topgrpplusgd  12658  topgrptsetd  12659  prdsex  12723  imasex  12731  imasival  12732  imasbas  12733  imasplusg  12734  imasmulr  12735  imasaddfnlemg  12740  imasaddvallemg  12741  xpsfval  12772  xpsval  12776  intopsn  12791  mgm1  12794  sgrp1  12821  mnd1  12852  mnd1id  12853  grp1  12981  grp1inv  12982  ring1  13241  txlm  13864