Theorem opexg 4368

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 3902	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ = {{𝐴}, {𝐴, 𝐵}})
2		elex 2833	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
3		snexg 4321	. . . . 5 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
4	2, 3	syl 14	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
5	4	adantr 276	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴} ∈ V)
6		elex 2833	. . . 4 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
7		prexg 4349	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
8	2, 6, 7	syl2an 289	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
9		prexg 4349	. . 3 ⊢ (({𝐴} ∈ V ∧ {𝐴, 𝐵} ∈ V) → {{𝐴}, {𝐴, 𝐵}} ∈ V)
10	5, 8, 9	syl2anc 415	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {{𝐴}, {𝐴, 𝐵}} ∈ V)
11	1, 10	eqeltrd 2315	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  Vcvv 2821  {csn 3709  {cpr 3710  ⟨cop 3712

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-pow 4311  ax-pr 4346

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718

This theorem is used by:  opex  4369  otexg  4370  opeliunxp  4830  opbrop  4854  relsnopg  4879  opswapg  5274  elxp4  5275  elxp5  5276  resfunexg  5936  fliftel  5999  fliftel1  6000  oprabid  6117  ovexg  6119  ovssunirng  6120  eloprabga  6175  op1st  6380  op2nd  6381  ot1stg  6386  ot2ndg  6387  ot3rdgg  6388  elxp6  6403  mpofvex  6441  algrflem  6465  algrflemg  6466  mpoxopoveq  6511  brtposg  6525  tfr0dm  6593  tfrlemisucaccv  6596  tfrlemibxssdm  6598  tfrlemibfn  6599  tfrlemi14d  6604  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemres  6620  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemres  6633  mapsnend  7099  en2prd  7106  fnfi  7250  snopfsuppdc  7299  djulclb  7396  inl11  7406  1stinl  7415  2ndinl  7416  1stinr  7417  2ndinr  7418  mulpipq2  7739  enq0breq  7804  addvalex  8212  peano2nnnn  8221  axcnre  8249  frec2uzrdg  10860  frecuzrdg0  10864  frecuzrdgg  10867  frecuzrdg0t  10873  zfz1isolem1  11307  s1leng  11407  s111  11414  pfxclz  11466  eucalgval2  12849  crth  13024  phimullem  13025  ennnfonelemp1  13348  setsvala  13434  setsex  13435  setsfun  13438  setsfun0  13439  setsresg  13441  setscom  13443  strslfv  13448  strslfv3  13449  setsslid  13454  bassetsnn  13460  strle1g  13511  1strbas  13522  2strbasg  13525  2stropg  13526  2strbas1g  13528  2strop1g  13529  rngbaseg  13541  rngplusgg  13542  rngmulrg  13543  srngbased  13552  srngplusgd  13553  srngmulrd  13554  srnginvld  13555  lmodbased  13570  lmodplusgd  13571  lmodscad  13572  lmodvscad  13573  ipsbased  13582  ipsaddgd  13583  ipsmulrd  13584  ipsscad  13585  ipsvscad  13586  ipsipd  13587  topgrpbasd  13602  topgrpplusgd  13603  topgrptsetd  13604  imasex  13677  imasival  13678  imasbas  13679  imasplusg  13680  imasmulr  13681  imasaddfnlemg  13686  imasaddvallemg  13687  xpsfval  13720  intopsn  13738  mgm1  13741  sgrp1  13777  mnd1  13813  mnd1id  13814  grp1  13962  grp1inv  13963  prdsex  14223  prdsval  14224  xpsval  14252  ring1  14415  psrval  15101  fnpsr  15102  psrbasg  15117  psrplusgg  15121  txlm  15432  struct2slots2dom  16401  structvtxval  16402  structiedg0val  16403  structgrssvtx  16405  structgrssiedg  16406  gropd  16410  edgopval  16425  edgstruct  16427  isuhgropm  16444  uhgrunop  16450  upgrop  16467  upgr0eop  16485  upgr1eopdc  16486  upgr1een  16487  umgr1een  16488  upgrunop  16490  umgrunop  16492  isuspgropen  16527  isusgropen  16528  ausgrusgrben  16531  usgr0eop  16605  uspgr1eopdc  16606  usgr1eop  16608  uhgrspanop  16645  vtxdgop  16655  p1evtxdeqfilem  16674  p1evtxdeqfi  16675  p1evtxdp1fi  16676  eupthvdres  16838  eupth2lem3fi  16839  konigsbergumgr  16850