Theorem uniex 7761

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

Syntax hints:   ∈ wcel 2108  Vcvv 3480  ∪ cuni 4907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908

This theorem is referenced by:  unexOLD  7765  iunpw  7791  elxp4  7944  elxp5  7945  1stval  8016  2ndval  8017  fo1st  8034  fo2nd  8035  cnvf1o  8136  brtpos2  8257  naddcllem  8714  ixpsnf1o  8978  dffi3  9471  cnfcom2  9742  cnfcom3lem  9743  cnfcom3  9744  ttrclse  9767  trcl  9768  rankc2  9911  rankxpl  9915  rankxpsuc  9922  acnlem  10088  dfac2a  10170  fin23lem14  10373  fin23lem16  10375  fin23lem17  10378  fin23lem38  10389  fin23lem39  10390  itunisuc  10459  axdc3lem2  10491  axcclem  10497  ac5b  10518  ttukey  10558  wunex2  10778  wuncval2  10787  intgru  10854  pnfex  11314  prdsvallem  17499  prdsval  17500  prdsds  17509  wunfunc  17946  wunnat  18004  arwval  18088  catcfuccl  18163  catcxpccl  18252  zrhval  21518  mreclatdemoBAD  23104  ptbasin2  23586  ptbasfi  23589  dfac14  23626  ptcmplem2  24061  ptcmplem3  24062  ptcmp  24066  cnextfvval  24073  cnextcn  24075  minveclem4a  25464  oldf  27896  madefi  27950  precsexlem10  28240  xrge0tsmsbi  33066  dimval  33651  dimvalfi  33652  locfinreflem  33839  pstmfval  33895  pstmxmet  33896  esumex  34030  msrval  35543  dfrdg2  35796  fvbigcup  35903  ctbssinf  37407  ptrest  37626  heiborlem1  37818  heiborlem3  37820  heibor  37828  dicval  41178  prjcrvfval  42641  aomclem1  43066  dfac21  43078  ntrrn  44135  ntrf  44136  dssmapntrcls  44141  fourierdlem70  46191  caragendifcl  46529  cnfsmf  46755  tposideq  48788  setrec1lem3  49208  setrec2fun  49211