Theorem uniex 7735

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

Syntax hints:   ∈ wcel 2108  Vcvv 3459  ∪ cuni 4883

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 2707  ax-sep 5266  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-uni 4884

This theorem is referenced by:  unexOLD  7739  iunpw  7765  elxp4  7918  elxp5  7919  1stval  7990  2ndval  7991  fo1st  8008  fo2nd  8009  cnvf1o  8110  brtpos2  8231  naddcllem  8688  ixpsnf1o  8952  dffi3  9443  cnfcom2  9716  cnfcom3lem  9717  cnfcom3  9718  ttrclse  9741  trcl  9742  rankc2  9885  rankxpl  9889  rankxpsuc  9896  acnlem  10062  dfac2a  10144  fin23lem14  10347  fin23lem16  10349  fin23lem17  10352  fin23lem38  10363  fin23lem39  10364  itunisuc  10433  axdc3lem2  10465  axcclem  10471  ac5b  10492  ttukey  10532  wunex2  10752  wuncval2  10761  intgru  10828  pnfex  11288  prdsvallem  17468  prdsval  17469  prdsds  17478  wunfunc  17914  wunnat  17972  arwval  18056  catcfuccl  18131  catcxpccl  18219  zrhval  21468  mreclatdemoBAD  23034  ptbasin2  23516  ptbasfi  23519  dfac14  23556  ptcmplem2  23991  ptcmplem3  23992  ptcmp  23996  cnextfvval  24003  cnextcn  24005  minveclem4a  25382  oldf  27817  madefi  27876  precsexlem10  28170  xrge0tsmsbi  33057  dimval  33640  dimvalfi  33641  locfinreflem  33871  pstmfval  33927  pstmxmet  33928  esumex  34060  msrval  35560  dfrdg2  35813  fvbigcup  35920  ctbssinf  37424  ptrest  37643  heiborlem1  37835  heiborlem3  37837  heibor  37845  dicval  41195  prjcrvfval  42654  aomclem1  43078  dfac21  43090  ntrrn  44146  ntrf  44147  dssmapntrcls  44152  permaxun  45036  fourierdlem70  46205  caragendifcl  46543  cnfsmf  46769  tposideq  48863  setrec1lem3  49553  setrec2fun  49556