Theorem uniex 7688

Description: The Axiom of Union in class notation. This says that if 𝐴 is a set i.e. 𝐴 ∈ V (see isset 3455), 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

Step	Hyp	Ref	Expression
1		uniex.1	. 2 ⊢ 𝐴 ∈ V
2		uniexg 7687	. 2 ⊢ (𝐴 ∈ V → ∪ 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ ∪ 𝐴 ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3441  ∪ cuni 4864

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 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-ss 3919  df-uni 4865

This theorem is referenced by:  unexOLD  7692  iunpw  7718  elxp4  7866  elxp5  7867  1stval  7937  2ndval  7938  fo1st  7955  fo2nd  7956  cnvf1o  8055  brtpos2  8176  naddcllem  8606  ixpsnf1o  8880  dffi3  9338  cnfcom2  9615  cnfcom3lem  9616  cnfcom3  9617  ttrclse  9640  trcl  9641  rankc2  9787  rankxpl  9791  rankxpsuc  9798  acnlem  9962  dfac2a  10044  fin23lem14  10247  fin23lem16  10249  fin23lem17  10252  fin23lem38  10263  fin23lem39  10264  itunisuc  10333  axdc3lem2  10365  axcclem  10371  ac5b  10392  ttukey  10432  wunex2  10653  wuncval2  10662  intgru  10729  pnfex  11189  prdsvallem  17378  prdsval  17379  prdsds  17388  wunfunc  17829  wunnat  17887  arwval  17971  catcfuccl  18046  catcxpccl  18134  zrhval  21466  mreclatdemoBAD  23044  ptbasin2  23526  ptbasfi  23529  dfac14  23566  ptcmplem2  24001  ptcmplem3  24002  ptcmp  24006  cnextfvval  24013  cnextcn  24015  minveclem4a  25390  oldf  27837  madefi  27913  precsexlem10  28216  xrge0tsmsbi  33158  dimval  33759  dimvalfi  33760  locfinreflem  33999  pstmfval  34055  pstmxmet  34056  esumex  34188  msrval  35734  dfrdg2  35989  fvbigcup  36096  ctbssinf  37613  ptrest  37822  heiborlem1  38014  heiborlem3  38016  heibor  38024  dicval  41504  prjcrvfval  42941  aomclem1  43363  dfac21  43375  ntrrn  44430  ntrf  44431  dssmapntrcls  44436  permaxun  45319  fourierdlem70  46487  caragendifcl  46825  cnfsmf  47051  tposideq  49200  setrec1lem3  50001  setrec2fun  50004