Theorem opexg 4349

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  Vcvv 2815  {csn 3694  {cpr 3695  ⟨cop 3697

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703

This theorem is referenced by:  opex  4350  otexg  4351  opeliunxp  4810  opbrop  4834  relsnopg  4859  opswapg  5254  elxp4  5255  elxp5  5256  resfunexg  5910  fliftel  5972  fliftel1  5973  oprabid  6090  ovexg  6092  ovssunirng  6093  eloprabga  6148  op1st  6353  op2nd  6354  ot1stg  6359  ot2ndg  6360  ot3rdgg  6361  elxp6  6376  mpofvex  6414  algrflem  6438  algrflemg  6439  mpoxopoveq  6484  brtposg  6498  tfr0dm  6566  tfrlemisucaccv  6569  tfrlemibxssdm  6571  tfrlemibfn  6572  tfrlemi14d  6577  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfr1onlemres  6593  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllembfn  6601  tfrcllemres  6606  mapsnend  7065  en2prd  7072  fnfi  7216  snopfsuppdc  7265  djulclb  7359  inl11  7369  1stinl  7378  2ndinl  7379  1stinr  7380  2ndinr  7381  mulpipq2  7702  enq0breq  7767  addvalex  8175  peano2nnnn  8184  axcnre  8212  frec2uzrdg  10798  frecuzrdg0  10802  frecuzrdgg  10805  frecuzrdg0t  10811  zfz1isolem1  11240  s1leng  11340  s111  11347  pfxclz  11399  eucalgval2  12779  crth  12950  phimullem  12951  ennnfonelemp1  13245  setsvala  13331  setsex  13332  setsfun  13335  setsfun0  13336  setsresg  13338  setscom  13340  strslfv  13345  strslfv3  13346  setsslid  13351  bassetsnn  13357  strle1g  13407  1strbas  13418  2strbasg  13421  2stropg  13422  2strbas1g  13424  2strop1g  13425  rngbaseg  13437  rngplusgg  13438  rngmulrg  13439  srngbased  13448  srngplusgd  13449  srngmulrd  13450  srnginvld  13451  lmodbased  13466  lmodplusgd  13467  lmodscad  13468  lmodvscad  13469  ipsbased  13478  ipsaddgd  13479  ipsmulrd  13480  ipsscad  13481  ipsvscad  13482  ipsipd  13483  topgrpbasd  13498  topgrpplusgd  13499  topgrptsetd  13500  imasex  13573  imasival  13574  imasbas  13575  imasplusg  13576  imasmulr  13577  imasaddfnlemg  13582  imasaddvallemg  13583  xpsfval  13616  intopsn  13634  mgm1  13637  sgrp1  13678  mnd1  13714  mnd1id  13715  grp1  13865  grp1inv  13866  prdsex  14118  prdsval  14119  xpsval  14147  ring1  14306  psrval  14944  fnpsr  14945  psrbasg  14959  psrplusgg  14963  txlm  15274  struct2slots2dom  16163  structvtxval  16164  structiedg0val  16165  structgrssvtx  16167  structgrssiedg  16168  gropd  16172  edgopval  16187  edgstruct  16189  isuhgropm  16206  uhgrunop  16212  upgrop  16229  upgr0eop  16247  upgr1eopdc  16248  upgr1een  16249  umgr1een  16250  upgrunop  16252  umgrunop  16254  isuspgropen  16289  isusgropen  16290  ausgrusgrben  16293  usgr0eop  16367  uspgr1eopdc  16368  usgr1eop  16370  uhgrspanop  16407  vtxdgop  16417  p1evtxdeqfilem  16436  p1evtxdeqfi  16437  p1evtxdp1fi  16438  eupthvdres  16600  eupth2lem3fi  16601  konigsbergumgr  16612