Theorem uniex 7692

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  ∪ cuni 4851

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 5232  ax-un 7686

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 3432  df-ss 3907  df-uni 4852

This theorem is referenced by:  unexOLD  7696  iunpw  7722  elxp4  7870  elxp5  7871  1stval  7941  2ndval  7942  fo1st  7959  fo2nd  7960  cnvf1o  8058  brtpos2  8179  naddcllem  8609  ixpsnf1o  8883  dffi3  9341  cnfcom2  9620  cnfcom3lem  9621  cnfcom3  9622  ttrclse  9645  trcl  9646  rankc2  9792  rankxpl  9796  rankxpsuc  9803  acnlem  9967  dfac2a  10049  fin23lem14  10252  fin23lem16  10254  fin23lem17  10257  fin23lem38  10268  fin23lem39  10269  itunisuc  10338  axdc3lem2  10370  axcclem  10376  ac5b  10397  ttukey  10437  wunex2  10658  wuncval2  10667  intgru  10734  pnfex  11195  prdsvallem  17414  prdsval  17415  prdsds  17424  wunfunc  17865  wunnat  17923  arwval  18007  catcfuccl  18082  catcxpccl  18170  zrhval  21503  mreclatdemoBAD  23077  ptbasin2  23559  ptbasfi  23562  dfac14  23599  ptcmplem2  24034  ptcmplem3  24035  ptcmp  24039  cnextfvval  24046  cnextcn  24048  minveclem4a  25413  oldf  27849  madefi  27925  precsexlem10  28228  xrge0tsmsbi  33156  dimval  33766  dimvalfi  33767  locfinreflem  34006  pstmfval  34062  pstmxmet  34063  esumex  34195  msrval  35742  dfrdg2  35997  fvbigcup  36104  ttctr  36697  ttcmin  36700  dfttc2g  36710  ctbssinf  37744  ptrest  37962  heiborlem1  38154  heiborlem3  38156  heibor  38164  dicval  41644  prjcrvfval  43086  aomclem1  43508  dfac21  43520  ntrrn  44575  ntrf  44576  dssmapntrcls  44581  permaxun  45464  fourierdlem70  46630  caragendifcl  46968  cnfsmf  47194  tposideq  49383  setrec1lem3  50184  setrec2fun  50187