MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  unex Structured version   Unicode version

Theorem unex 6580
Description: The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 1-Jul-1994.)
Hypotheses
Ref Expression
unex.1  |-  A  e. 
_V
unex.2  |-  B  e. 
_V
Assertion
Ref Expression
unex  |-  ( A  u.  B )  e. 
_V

Proof of Theorem unex
StepHypRef Expression
1 unex.1 . . 3  |-  A  e. 
_V
2 unex.2 . . 3  |-  B  e. 
_V
31, 2unipr 4258 . 2  |-  U. { A ,  B }  =  ( A  u.  B )
4 prex 4689 . . 3  |-  { A ,  B }  e.  _V
54uniex 6578 . 2  |-  U. { A ,  B }  e.  _V
63, 5eqeltrri 2552 1  |-  ( A  u.  B )  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767   _Vcvv 3113    u. cun 3474   {cpr 4029   U.cuni 4245
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686  ax-un 6574
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-rex 2820  df-v 3115  df-dif 3479  df-un 3481  df-nul 3786  df-sn 4028  df-pr 4030  df-uni 4246
This theorem is referenced by:  tpex  6581  unexb  6582  fvclex  6753  ralxpmap  7465  unen  7595  enfixsn  7623  sbthlem10  7633  unxpdomlem3  7723  isinf  7730  findcard2  7756  ac6sfi  7760  pwfilem  7810  fiin  7878  cnfcomlem  8139  cnfcomlemOLD  8147  trcl  8155  tc2  8169  rankxpu  8290  rankxplim  8293  rankxplim3  8295  r0weon  8386  infxpenlem  8387  dfac4  8499  dfac2  8507  kmlem2  8527  cdafn  8545  cfsmolem  8646  isfin1-3  8762  axdc2lem  8824  axdc3lem4  8829  axcclem  8833  ttukeylem3  8887  gchac  9055  wunex2  9112  wuncval2  9121  inar1  9149  nn0ex  10797  xrex  11213  hashbclem  12463  ccatfn  12552  incexclem  13607  ramub1lem2  14400  prdsval  14706  imasval  14762  ipoval  15637  fpwipodrs  15647  plusffval  15740  staffval  17279  scaffval  17313  lpival  17675  psrval  17782  xrsex  18204  ipffval  18450  islindf4  18640  neitr  19447  leordtval2  19479  1stckgen  19790  dfac14  19854  ptcmpfi  20049  hausflim  20217  flimclslem  20220  alexsubALTlem2  20283  nmfval  20844  icccmplem2  21063  tchex  21395  tchnmfval  21406  taylfval  22488  legval  23698  axlowdimlem15  23935  axlowdim  23940  eengv  23958  constr3lem1  24321  constr3cyclpe  24339  3v3e3cycl2  24340  ordtconlem1  27542  sxbrsigalem2  27897  subfacp1lem3  28266  subfacp1lem5  28268  erdszelem8  28282  finixpnum  29615  comppfsc  29779  rrnval  29926  elrfi  30230  istopclsd  30236  mzpcompact2lem  30288  eldioph2lem1  30297  eldioph2lem2  30298  eldioph4b  30349  diophren  30351  ttac  30582  pwslnmlem2  30643  dfacbasgrp  30661  mendval  30737  idomsubgmo  30760  fnchoice  30982  limcresiooub  31184  limcresioolb  31185  fourierdlem48  31455  fourierdlem49  31456  fourierdlem102  31509  fourierdlem114  31521  bnj918  32903  lsatset  33787  ldualset  33922  pclfinN  34696  dvaset  35801  dvhset  35878  hlhilset  36734  superuncl  36773  ssuncl  36775  sssymdifcl  36777  trclubg  36795
  Copyright terms: Public domain W3C validator