Theorem opexg 4277

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2177  Vcvv 2773  {csn 3635  {cpr 3636  ⟨cop 3638

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2180  ax-ext 2188  ax-sep 4167  ax-pow 4223  ax-pr 4258

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3172  df-in 3174  df-ss 3181  df-pw 3620  df-sn 3641  df-pr 3642  df-op 3644

This theorem is referenced by:  opex  4278  otexg  4279  opeliunxp  4735  opbrop  4759  relsnopg  4784  opswapg  5175  elxp4  5176  elxp5  5177  resfunexg  5815  fliftel  5872  fliftel1  5873  oprabid  5986  ovexg  5988  ovssunirng  5989  eloprabga  6042  op1st  6242  op2nd  6243  ot1stg  6248  ot2ndg  6249  ot3rdgg  6250  elxp6  6265  mpofvex  6301  algrflem  6325  algrflemg  6326  mpoxopoveq  6336  brtposg  6350  tfr0dm  6418  tfrlemisucaccv  6421  tfrlemibxssdm  6423  tfrlemibfn  6424  tfrlemi14d  6429  tfr1onlemsucaccv  6437  tfr1onlembxssdm  6439  tfr1onlembfn  6440  tfr1onlemres  6445  tfrcllemsucaccv  6450  tfrcllembxssdm  6452  tfrcllembfn  6453  tfrcllemres  6458  en2prd  6920  fnfi  7050  djulclb  7169  inl11  7179  1stinl  7188  2ndinl  7189  1stinr  7190  2ndinr  7191  mulpipq2  7497  enq0breq  7562  addvalex  7970  peano2nnnn  7979  axcnre  8007  frec2uzrdg  10567  frecuzrdg0  10571  frecuzrdgg  10574  frecuzrdg0t  10580  zfz1isolem1  10998  s1leng  11092  s111  11099  eucalgval2  12425  crth  12596  phimullem  12597  ennnfonelemp1  12827  setsvala  12913  setsex  12914  setsfun  12917  setsfun0  12918  setsresg  12920  setscom  12922  strslfv  12927  strslfv3  12928  setsslid  12933  strle1g  12988  1strbas  12999  2strbasg  13002  2stropg  13003  2strbas1g  13005  2strop1g  13006  rngbaseg  13018  rngplusgg  13019  rngmulrg  13020  srngbased  13029  srngplusgd  13030  srngmulrd  13031  srnginvld  13032  lmodbased  13047  lmodplusgd  13048  lmodscad  13049  lmodvscad  13050  ipsbased  13059  ipsaddgd  13060  ipsmulrd  13061  ipsscad  13062  ipsvscad  13063  ipsipd  13064  topgrpbasd  13079  topgrpplusgd  13080  topgrptsetd  13081  prdsex  13151  prdsval  13155  imasex  13187  imasival  13188  imasbas  13189  imasplusg  13190  imasmulr  13191  imasaddfnlemg  13196  imasaddvallemg  13197  xpsfval  13230  xpsval  13234  intopsn  13249  mgm1  13252  sgrp1  13293  mnd1  13337  mnd1id  13338  grp1  13488  grp1inv  13489  ring1  13871  psrval  14478  fnpsr  14479  psrbasg  14486  psrplusgg  14490  txlm  14801  struct2slots2dom  15687  structvtxval  15688  structiedg0val  15689  structgrssvtx  15691  structgrssiedg  15692  gropd  15696  edgopval  15708  edgstruct  15710  isuhgropm  15727  uhgrunop  15733  upgrop  15750  upgr0eop  15765  upgr1eopdc  15766  upgrunop  15768  umgrunop  15770