Theorem opexg 4370

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 4323	. . . . 5 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
4	2, 3	syl 14	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
5	4	adantr 276	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴} ∈ V)
6		elex 2833	. . . 4 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
7		prexg 4351	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
8	2, 6, 7	syl2an 289	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
9		prexg 4351	. . 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 4251  ax-pow 4313  ax-pr 4348

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  4371  otexg  4372  opeliunxp  4832  opbrop  4856  relsnopg  4881  opswapg  5277  elxp4  5278  elxp5  5279  resfunexg  5939  fliftel  6002  fliftel1  6003  oprabid  6120  ovexg  6122  ovssunirng  6123  eloprabga  6178  op1st  6384  op2nd  6385  ot1stg  6390  ot2ndg  6391  ot3rdgg  6392  elxp6  6407  mpofvex  6445  algrflem  6469  algrflemg  6470  mpoxopoveq  6516  brtposg  6530  tfr0dm  6598  tfrlemisucaccv  6601  tfrlemibxssdm  6603  tfrlemibfn  6604  tfrlemi14d  6609  tfr1onlemsucaccv  6617  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfr1onlemres  6625  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllembfn  6633  tfrcllemres  6638  mapsnend  7105  en2prd  7112  fnfi  7256  snopfsupp  7307  djulclb  7402  inl11  7412  1stinl  7421  2ndinl  7422  1stinr  7423  2ndinr  7424  mulpipq2  7745  enq0breq  7810  addvalex  8218  peano2nnnn  8227  axcnre  8255  frec2uzrdg  10867  frecuzrdg0  10871  frecuzrdgg  10874  frecuzrdg0t  10880  zfz1isolem1  11314  s1leng  11414  s111  11421  pfxclz  11473  eucalgval2  12856  crth  13031  phimullem  13032  ennnfonelemp1  13355  setsvala  13441  setsex  13442  setsfun  13445  setsfun0  13446  setsresg  13448  setscom  13450  strslfv  13455  strslfv3  13456  setsslid  13461  bassetsnn  13467  strle1g  13519  1strbas  13530  2strbasg  13533  2stropg  13534  2strbas1g  13536  2strop1g  13537  rngbaseg  13549  rngplusgg  13550  rngmulrg  13551  srngbased  13560  srngplusgd  13561  srngmulrd  13562  srnginvld  13563  lmodbased  13578  lmodplusgd  13579  lmodscad  13580  lmodvscad  13581  ipsbased  13590  ipsaddgd  13591  ipsmulrd  13592  ipsscad  13593  ipsvscad  13594  ipsipd  13595  topgrpbasd  13610  topgrpplusgd  13611  topgrptsetd  13612  imasex  13685  imasival  13686  imasbas  13687  imasplusg  13688  imasmulr  13689  imasaddfnlemg  13694  imasaddvallemg  13695  xpsfval  13728  intopsn  13746  mgm1  13749  sgrp1  13785  mnd1  13821  mnd1id  13822  grp1  13970  grp1inv  13971  prdsex  14279  prdsval  14280  xpsval  14308  ring1  14471  psrval  15161  fnpsr  15162  psrbasg  15197  psrplusgg  15201  txlm  15538  struct2slots2dom  16517  structvtxval  16518  structiedg0val  16519  structgrssvtx  16521  structgrssiedg  16522  gropd  16526  edgopval  16541  edgstruct  16543  isuhgropm  16560  uhgrunop  16566  upgrop  16583  upgr0eop  16601  upgr1eopdc  16602  upgr1een  16603  umgr1een  16604  upgrunop  16606  umgrunop  16608  isuspgropen  16643  isusgropen  16644  ausgrusgrben  16647  usgr0eop  16721  uspgr1eopdc  16722  usgr1eop  16724  uhgrspanop  16761  vtxdgop  16771  p1evtxdeqfilem  16790  p1evtxdeqfi  16791  p1evtxdp1fi  16792  eupthvdres  16954  eupth2lem3fi  16955  konigsbergumgr  16966