Theorem uniex 7776

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-uni 4932

This theorem is referenced by:  unexOLD  7780  iunpw  7806  elxp4  7962  elxp5  7963  1stval  8032  2ndval  8033  fo1st  8050  fo2nd  8051  cnvf1o  8152  brtpos2  8273  naddcllem  8732  ixpsnf1o  8996  dffi3  9500  cnfcom2  9771  cnfcom3lem  9772  cnfcom3  9773  ttrclse  9796  trcl  9797  rankc2  9940  rankxpl  9944  rankxpsuc  9951  acnlem  10117  dfac2a  10199  fin23lem14  10402  fin23lem16  10404  fin23lem17  10407  fin23lem38  10418  fin23lem39  10419  itunisuc  10488  axdc3lem2  10520  axcclem  10526  ac5b  10547  ttukey  10587  wunex2  10807  wuncval2  10816  intgru  10883  pnfex  11343  prdsvallem  17514  prdsval  17515  prdsds  17524  wunfunc  17965  wunfuncOLD  17966  wunnat  18024  wunnatOLD  18025  arwval  18110  catcfuccl  18186  catcfucclOLD  18187  catcxpccl  18276  catcxpcclOLD  18277  zrhval  21541  mreclatdemoBAD  23125  ptbasin2  23607  ptbasfi  23610  dfac14  23647  ptcmplem2  24082  ptcmplem3  24083  ptcmp  24087  cnextfvval  24094  cnextcn  24096  minveclem4a  25483  oldf  27914  madefi  27968  precsexlem10  28258  xrge0tsmsbi  33042  dimval  33613  dimvalfi  33614  locfinreflem  33786  pstmfval  33842  pstmxmet  33843  esumex  33993  msrval  35506  dfrdg2  35759  fvbigcup  35866  ctbssinf  37372  ptrest  37579  heiborlem1  37771  heiborlem3  37773  heibor  37781  dicval  41133  prjcrvfval  42586  aomclem1  43011  dfac21  43023  ntrrn  44084  ntrf  44085  dssmapntrcls  44090  fourierdlem70  46097  caragendifcl  46435  cnfsmf  46661  setrec1lem3  48781  setrec2fun  48784