Theorem uniex 7677

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

Syntax hints:   ∈ wcel 2109  Vcvv 3436  ∪ cuni 4858

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-uni 4859

This theorem is referenced by:  unexOLD  7681  iunpw  7707  elxp4  7855  elxp5  7856  1stval  7926  2ndval  7927  fo1st  7944  fo2nd  7945  cnvf1o  8044  brtpos2  8165  naddcllem  8594  ixpsnf1o  8865  dffi3  9321  cnfcom2  9598  cnfcom3lem  9599  cnfcom3  9600  ttrclse  9623  trcl  9624  rankc2  9767  rankxpl  9771  rankxpsuc  9778  acnlem  9942  dfac2a  10024  fin23lem14  10227  fin23lem16  10229  fin23lem17  10232  fin23lem38  10243  fin23lem39  10244  itunisuc  10313  axdc3lem2  10345  axcclem  10351  ac5b  10372  ttukey  10412  wunex2  10632  wuncval2  10641  intgru  10708  pnfex  11168  prdsvallem  17358  prdsval  17359  prdsds  17368  wunfunc  17808  wunnat  17866  arwval  17950  catcfuccl  18025  catcxpccl  18113  zrhval  21414  mreclatdemoBAD  22981  ptbasin2  23463  ptbasfi  23466  dfac14  23503  ptcmplem2  23938  ptcmplem3  23939  ptcmp  23943  cnextfvval  23950  cnextcn  23952  minveclem4a  25328  oldf  27769  madefi  27829  precsexlem10  28125  xrge0tsmsbi  33025  dimval  33583  dimvalfi  33584  locfinreflem  33823  pstmfval  33879  pstmxmet  33880  esumex  34012  msrval  35531  dfrdg2  35789  fvbigcup  35896  ctbssinf  37400  ptrest  37619  heiborlem1  37811  heiborlem3  37813  heibor  37821  dicval  41175  prjcrvfval  42624  aomclem1  43047  dfac21  43059  ntrrn  44115  ntrf  44116  dssmapntrcls  44121  permaxun  45005  fourierdlem70  46177  caragendifcl  46515  cnfsmf  46741  tposideq  48892  setrec1lem3  49694  setrec2fun  49697