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

Theorem uniex 7683
Description: The Axiom of Union in class notation. This says that if 𝐴 is a set i.e. 𝐴 ∈ V (see isset 3461), 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 7682 . 2 (𝐴 ∈ V → 𝐴 ∈ V)
31, 2ax-mp 5 1 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  Vcvv 3448   cuni 4870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5261  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932  df-uni 4871
This theorem is referenced by:  unex  7685  iunpw  7710  elxp4  7864  elxp5  7865  1stval  7928  2ndval  7929  fo1st  7946  fo2nd  7947  cnvf1o  8048  brtpos2  8168  naddcllem  8627  ixpsnf1o  8883  dffi3  9374  cnfcom2  9645  cnfcom3lem  9646  cnfcom3  9647  ttrclse  9670  trcl  9671  rankc2  9814  rankxpl  9818  rankxpsuc  9825  acnlem  9991  dfac2a  10072  fin23lem14  10276  fin23lem16  10278  fin23lem17  10281  fin23lem38  10292  fin23lem39  10293  itunisuc  10362  axdc3lem2  10394  axcclem  10400  ac5b  10421  ttukey  10461  wunex2  10681  wuncval2  10690  intgru  10757  pnfex  11215  prdsvallem  17343  prdsval  17344  prdsds  17353  wunfunc  17792  wunfuncOLD  17793  wunnat  17850  wunnatOLD  17851  arwval  17936  catcfuccl  18012  catcfucclOLD  18013  catcxpccl  18102  catcxpcclOLD  18103  zrhval  20924  mreclatdemoBAD  22463  ptbasin2  22945  ptbasfi  22948  dfac14  22985  ptcmplem2  23420  ptcmplem3  23421  ptcmp  23425  cnextfvval  23432  cnextcn  23434  minveclem4a  24810  oldf  27209  xrge0tsmsbi  31942  dimval  32340  dimvalfi  32341  locfinreflem  32461  pstmfval  32517  pstmxmet  32518  esumex  32668  msrval  34172  dfrdg2  34409  fvbigcup  34516  ctbssinf  35906  ptrest  36106  heiborlem1  36299  heiborlem3  36301  heibor  36309  dicval  39668  prjcrvfval  40998  aomclem1  41410  dfac21  41422  ntrrn  42468  ntrf  42469  dssmapntrcls  42474  fourierdlem70  44491  caragendifcl  44829  cnfsmf  45055  setrec1lem3  47208  setrec2fun  47211
  Copyright terms: Public domain W3C validator