Theorem uniex 7697

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

Syntax hints:   ∈ wcel 2109  Vcvv 3444  ∪ cuni 4867

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 5246  ax-un 7691

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 3446  df-ss 3928  df-uni 4868

This theorem is referenced by:  unexOLD  7701  iunpw  7727  elxp4  7878  elxp5  7879  1stval  7949  2ndval  7950  fo1st  7967  fo2nd  7968  cnvf1o  8067  brtpos2  8188  naddcllem  8617  ixpsnf1o  8888  dffi3  9358  cnfcom2  9633  cnfcom3lem  9634  cnfcom3  9635  ttrclse  9658  trcl  9659  rankc2  9802  rankxpl  9806  rankxpsuc  9813  acnlem  9979  dfac2a  10061  fin23lem14  10264  fin23lem16  10266  fin23lem17  10269  fin23lem38  10280  fin23lem39  10281  itunisuc  10350  axdc3lem2  10382  axcclem  10388  ac5b  10409  ttukey  10449  wunex2  10669  wuncval2  10678  intgru  10745  pnfex  11205  prdsvallem  17394  prdsval  17395  prdsds  17404  wunfunc  17844  wunnat  17902  arwval  17986  catcfuccl  18061  catcxpccl  18149  zrhval  21450  mreclatdemoBAD  23017  ptbasin2  23499  ptbasfi  23502  dfac14  23539  ptcmplem2  23974  ptcmplem3  23975  ptcmp  23979  cnextfvval  23986  cnextcn  23988  minveclem4a  25364  oldf  27803  madefi  27863  precsexlem10  28159  xrge0tsmsbi  33047  dimval  33590  dimvalfi  33591  locfinreflem  33824  pstmfval  33880  pstmxmet  33881  esumex  34013  msrval  35519  dfrdg2  35777  fvbigcup  35884  ctbssinf  37388  ptrest  37607  heiborlem1  37799  heiborlem3  37801  heibor  37809  dicval  41164  prjcrvfval  42613  aomclem1  43037  dfac21  43049  ntrrn  44105  ntrf  44106  dssmapntrcls  44111  permaxun  44995  fourierdlem70  46168  caragendifcl  46506  cnfsmf  46732  tposideq  48870  setrec1lem3  49672  setrec2fun  49675