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

Theorem uniex 4705
Description: The Axiom of Union in class notation. This says that if 
A is a set i.e.  A  e.  _V (see isset 2960), 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 4024 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
32eleq1d 2502 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
4 uniex2 4704 . . 3  |-  E. y 
y  =  U. x
54issetri 2963 . 2  |-  U. x  e.  _V
61, 3, 5vtocl 3006 1  |-  U. A  e.  _V
Colors of variables: wff set class
Syntax hints:    = wceq 1652    e. wcel 1725   _Vcvv 2956   U.cuni 4015
This theorem is referenced by:  uniexg  4706  unex  4707  uniuni  4716  iunpw  4759  elxp4  5357  elxp5  5358  1stval  6351  2ndval  6352  fo1st  6366  fo2nd  6367  cnvf1o  6445  brtpos2  6485  ixpsnf1o  7102  dffi3  7436  cnfcom2  7659  cnfcom3lem  7660  cnfcom3  7661  trcl  7664  rankuni  7789  rankc2  7797  rankxpl  7801  rankxpsuc  7806  r0weon  7894  acnlem  7929  dfac3  8002  dfac5lem4  8007  dfac2a  8010  dfac8  8015  dfacacn  8021  kmlem2  8031  cfslb2n  8148  fin23lem14  8213  fin23lem16  8215  fin23lem17  8218  fin23lem38  8229  fin23lem39  8230  itunisuc  8299  axdc3lem2  8331  axcclem  8337  ac5b  8358  ttukeylem5  8393  ttukeylem6  8394  ttukey  8398  brdom7disj  8409  brdom6disj  8410  intwun  8610  wunex2  8613  wuncval2  8622  intgru  8689  pnfxr  10713  prdsval  13678  prdsds  13686  fnmrc  13832  mrcfval  13833  mrisval  13855  wunfunc  14096  wunnat  14153  arwval  14198  catcfuccl  14264  catcxpccl  14304  sylow2a  15253  zrhval  16789  distop  17060  fctop  17068  cctop  17070  ppttop  17071  epttop  17073  fncld  17086  mretopd  17156  toponmre  17157  mreclatdemo  17160  iscnp2  17303  2ndcsep  17522  kgenf  17573  ptbasin2  17610  ptbasfi  17613  dfac14  17650  alexsubALTlem2  18079  ptcmplem2  18084  ptcmplem3  18085  ptcmp  18089  cnextfvval  18096  cnextcn  18098  minveclem4a  19331  xrge0tsmsbi  24224  pstmfval  24291  pstmxmet  24292  esumex  24426  pwsiga  24513  sigainb  24519  dmsigagen  24527  dfrdg2  25423  trpredex  25515  fvbigcup  25747  brapply  25783  dfrdg4  25795  mbfresfi  26253  fnessref  26373  neibastop1  26388  heiborlem1  26520  heiborlem3  26522  heibor  26530  aomclem1  27129  dfac21  27141  dicval  31974
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330  ax-un 4701
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rex 2711  df-v 2958  df-uni 4016
  Copyright terms: Public domain W3C validator