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

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

Proof of Theorem uniex
StepHypRef Expression
1 uniex.1 . 2 𝐴 ∈ V
2 uniexg 7461 . 2 (𝐴 ∈ V → 𝐴 ∈ V)
31, 2ax-mp 5 1 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2115  Vcvv 3481   cuni 4825
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796  ax-sep 5190  ax-un 7456
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3483  df-in 3927  df-ss 3937  df-uni 4826
This theorem is referenced by:  unex  7464  iunpw  7488  elxp4  7623  elxp5  7624  1stval  7687  2ndval  7688  fo1st  7705  fo2nd  7706  cnvf1o  7803  brtpos2  7895  ixpsnf1o  8499  dffi3  8893  cnfcom2  9163  cnfcom3lem  9164  cnfcom3  9165  trcl  9168  rankc2  9298  rankxpl  9302  rankxpsuc  9309  acnlem  9473  dfac2a  9554  fin23lem14  9754  fin23lem16  9756  fin23lem17  9759  fin23lem38  9770  fin23lem39  9771  itunisuc  9840  axdc3lem2  9872  axcclem  9878  ac5b  9899  ttukey  9939  wunex2  10159  wuncval2  10168  intgru  10235  pnfex  10693  prdsval  16731  prdsds  16740  wunfunc  17172  wunnat  17229  arwval  17306  catcfuccl  17372  catcxpccl  17460  zrhval  20658  mreclatdemoBAD  21707  ptbasin2  22189  ptbasfi  22192  dfac14  22229  ptcmplem2  22664  ptcmplem3  22665  ptcmp  22669  cnextfvval  22676  cnextcn  22678  minveclem4a  24040  xrge0tsmsbi  30728  dimval  31064  dimvalfi  31065  locfinreflem  31167  pstmfval  31199  pstmxmet  31200  esumex  31348  msrval  32845  dfrdg2  33100  trpredex  33136  fvbigcup  33423  ctbssinf  34771  ptrest  35002  heiborlem1  35195  heiborlem3  35197  heibor  35205  dicval  38418  aomclem1  39915  dfac21  39927  ntrrn  40745  ntrf  40746  dssmapntrcls  40751  fourierdlem70  42745  caragendifcl  43080  cnfsmf  43301  setrec1lem3  45146  setrec2fun  45149
  Copyright terms: Public domain W3C validator