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

Theorem uniex 6574
Description: The Axiom of Union in class notation. This says that if 
A is a set i.e.  A  e.  _V (see isset 3016), then the union of  A is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16. (Contributed by NM, 11-Aug-1993.)
Hypothesis
Ref Expression
uniex.1  |-  A  e. 
_V
Assertion
Ref Expression
uniex  |-  U. A  e.  _V

Proof of Theorem uniex
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uniex.1 . 2  |-  A  e. 
_V
2 unieq 4175 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
32eleq1d 2513 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
4 uniex2 6573 . . 3  |-  E. y 
y  =  U. x
54issetri 3019 . 2  |-  U. x  e.  _V
61, 3, 5vtocl 3067 1  |-  U. A  e.  _V
Colors of variables: wff setvar class
Syntax hints:    = wceq 1447    e. wcel 1890   _Vcvv 3012   U.cuni 4167
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-sep 4496  ax-un 6570
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rex 2742  df-v 3014  df-uni 4168
This theorem is referenced by:  uniexg  6575  unex  6576  uniuni  6587  iunpw  6592  elxp4  6724  elxp5  6725  1stval  6782  2ndval  6783  fo1st  6800  fo2nd  6801  cnvf1o  6882  brtpos2  6965  ixpsnf1o  7548  dffi3  7931  cnfcom2  8193  cnfcom3lem  8194  cnfcom3  8195  trcl  8198  rankuni  8320  rankc2  8328  rankxpl  8332  rankxpsuc  8339  r0weon  8429  acnlem  8465  dfac3  8538  dfac5lem4  8543  dfac2a  8546  dfac8  8551  dfacacn  8557  kmlem2  8567  cfslb2n  8684  fin23lem14  8749  fin23lem16  8751  fin23lem17  8754  fin23lem38  8765  fin23lem39  8766  itunisuc  8835  axdc3lem2  8867  axcclem  8873  ac5b  8894  ttukeylem5  8929  ttukeylem6  8930  ttukey  8934  brdom7disj  8945  brdom6disj  8946  intwun  9146  wunex2  9149  wuncval2  9158  intgru  9225  pnfxr  11401  prdsval  15363  prdsds  15372  fnmrc  15523  mrcfval  15524  mrisval  15546  wunfunc  15814  wunnat  15871  arwval  15948  catcfuccl  16014  catcxpccl  16102  sylow2a  17281  zrhval  19089  distop  20021  fctop  20029  cctop  20031  ppttop  20032  epttop  20034  fncld  20047  mretopd  20118  toponmre  20119  mreclatdemoBAD  20122  iscnp2  20265  2ndcsep  20484  kgenf  20566  ptbasin2  20603  ptbasfi  20606  dfac14  20643  alexsubALTlem2  21073  ptcmplem2  21078  ptcmplem3  21079  ptcmp  21083  cnextfvval  21090  cnextcn  21092  minveclem4a  22382  minveclem4aOLD  22394  xrge0tsmsbi  28555  locfinreflem  28673  pstmfval  28705  pstmxmet  28706  esumex  28856  pwsiga  28958  sigainb  28964  dmsigagen  28972  pwldsys  28985  ldsysgenld  28988  ldgenpisyslem1  28991  ddemeas  29064  msrval  30181  dfrdg2  30447  trpredex  30483  fvbigcup  30674  brapply  30710  dfrdg4  30723  fnessref  31018  neibastop1  31020  finxpreclem2  31783  ptrest  31940  mbfresfi  31988  heiborlem1  32144  heiborlem3  32146  heibor  32154  dicval  34745  aomclem1  35913  dfac21  35925  pwinfi  36169  fourierdlem70  38096  pwsal  38232  intsal  38245  salexct  38249  caragendifcl  38398  0ome  38413
  Copyright terms: Public domain W3C validator