Theorem uniex 7594

Description: The Axiom of Union in class notation. This says that if 𝐴 is a set i.e. 𝐴 ∈ V (see isset 3445), 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 7593	. 2 ⊢ (𝐴 ∈ V → ∪ 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ ∪ 𝐴 ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3432  ∪ cuni 4839

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840

This theorem is referenced by:  unex  7596  iunpw  7621  elxp4  7769  elxp5  7770  1stval  7833  2ndval  7834  fo1st  7851  fo2nd  7852  cnvf1o  7951  brtpos2  8048  ixpsnf1o  8726  dffi3  9190  cnfcom2  9460  cnfcom3lem  9461  cnfcom3  9462  ttrclse  9485  trcl  9486  rankc2  9629  rankxpl  9633  rankxpsuc  9640  acnlem  9804  dfac2a  9885  fin23lem14  10089  fin23lem16  10091  fin23lem17  10094  fin23lem38  10105  fin23lem39  10106  itunisuc  10175  axdc3lem2  10207  axcclem  10213  ac5b  10234  ttukey  10274  wunex2  10494  wuncval2  10503  intgru  10570  pnfex  11028  prdsvallem  17165  prdsval  17166  prdsds  17175  wunfunc  17614  wunfuncOLD  17615  wunnat  17672  wunnatOLD  17673  arwval  17758  catcfuccl  17834  catcfucclOLD  17835  catcxpccl  17924  catcxpcclOLD  17925  zrhval  20709  mreclatdemoBAD  22247  ptbasin2  22729  ptbasfi  22732  dfac14  22769  ptcmplem2  23204  ptcmplem3  23205  ptcmp  23209  cnextfvval  23216  cnextcn  23218  minveclem4a  24594  xrge0tsmsbi  31318  dimval  31686  dimvalfi  31687  locfinreflem  31790  pstmfval  31846  pstmxmet  31847  esumex  31997  msrval  33500  dfrdg2  33771  naddcllem  33831  oldf  34041  fvbigcup  34204  ctbssinf  35577  ptrest  35776  heiborlem1  35969  heiborlem3  35971  heibor  35979  dicval  39190  prjcrvfval  40468  aomclem1  40879  dfac21  40891  ntrrn  41732  ntrf  41733  dssmapntrcls  41738  fourierdlem70  43717  caragendifcl  44052  cnfsmf  44276  setrec1lem3  46395  setrec2fun  46398