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

Theorem uniex 4488
Description: The Axiom of Union in class notation. This says that if 
A is a set i.e.  A  e.  _V (see isset 2767), 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
StepHypRef Expression
1 uniex.1 . 2  |-  A  e. 
_V
2 unieq 3810 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
32eleq1d 2324 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
4 uniex2 4487 . . 3  |-  E. y 
y  =  U. x
54issetri 2770 . 2  |-  U. x  e.  _V
61, 3, 5vtocl 2813 1  |-  U. A  e.  _V
Colors of variables: wff set class
Syntax hints:    = wceq 1619    e. wcel 1621   _Vcvv 2763   U.cuni 3801
This theorem is referenced by:  uniexg  4489  unex  4490  uniuni  4499  iunpw  4542  elxp4  5147  elxp5  5148  fvex  5472  1stval  6058  2ndval  6059  fo1st  6073  fo2nd  6074  cnvf1o  6151  brtpos2  6174  ixpsnf1o  6824  dffi3  7152  cnfcom2  7373  cnfcom3lem  7374  cnfcom3  7375  trcl  7378  rankuni  7503  rankc2  7511  rankxpl  7515  rankxpsuc  7520  r0weon  7608  acnlem  7643  dfac3  7716  dfac5lem4  7721  dfac2a  7724  dfac8  7729  dfacacn  7735  kmlem2  7745  cfslb2n  7862  fin23lem14  7927  fin23lem16  7929  fin23lem17  7932  fin23lem38  7943  fin23lem39  7944  itunisuc  8013  axdc3lem2  8045  axcclem  8051  ac5b  8073  ttukeylem5  8108  ttukeylem6  8109  ttukey  8113  brdom7disj  8124  brdom6disj  8125  intwun  8325  wunex2  8328  wuncval2  8337  intgru  8404  pnfxr  10423  prdsval  13318  prdsds  13326  fnmrc  13472  mrcfval  13473  mrisval  13495  wunfunc  13736  wunnat  13793  arwval  13838  catcfuccl  13904  catcxpccl  13944  sylow2a  14893  zrhval  16425  distop  16696  fctop  16704  cctop  16706  ppttop  16707  epttop  16709  fncld  16722  mretopd  16792  toponmre  16793  mreclatdemo  16796  iscnp2  16932  2ndcsep  17148  kgenf  17199  ptbasin2  17236  ptbasfi  17239  dfac14  17275  alexsubALTlem2  17705  ptcmplem2  17710  ptcmplem3  17711  ptcmp  17715  minveclem4a  18757  dfrdg2  23522  trpredex  23610  fvbigcup  23819  brapply  23853  dfrdg4  23864  toplat  24658  inttop2  24883  qusp  24910  usptoplem  24914  istopx  24915  prcnt  24919  limvinlv  24927  fnessref  25661  neibastop1  25676  heiborlem1  25903  heiborlem3  25905  heibor  25913  aomclem1  26519  dfac21  26532  dicval  30616
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-un 4484
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-rex 2524  df-v 2765  df-uni 3802
  Copyright terms: Public domain W3C validator