Theorem uniex 7674

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 7673	. 2 ⊢ (𝐴 ∈ V → ∪ 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ ∪ 𝐴 ∈ V

Syntax hints:   ∈ wcel 2111  Vcvv 3436  ∪ cuni 4856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-uni 4857

This theorem is referenced by:  unexOLD  7678  iunpw  7704  elxp4  7852  elxp5  7853  1stval  7923  2ndval  7924  fo1st  7941  fo2nd  7942  cnvf1o  8041  brtpos2  8162  naddcllem  8591  ixpsnf1o  8862  dffi3  9315  cnfcom2  9592  cnfcom3lem  9593  cnfcom3  9594  ttrclse  9617  trcl  9618  rankc2  9764  rankxpl  9768  rankxpsuc  9775  acnlem  9939  dfac2a  10021  fin23lem14  10224  fin23lem16  10226  fin23lem17  10229  fin23lem38  10240  fin23lem39  10241  itunisuc  10310  axdc3lem2  10342  axcclem  10348  ac5b  10369  ttukey  10409  wunex2  10629  wuncval2  10638  intgru  10705  pnfex  11165  prdsvallem  17358  prdsval  17359  prdsds  17368  wunfunc  17808  wunnat  17866  arwval  17950  catcfuccl  18025  catcxpccl  18113  zrhval  21444  mreclatdemoBAD  23011  ptbasin2  23493  ptbasfi  23496  dfac14  23533  ptcmplem2  23968  ptcmplem3  23969  ptcmp  23973  cnextfvval  23980  cnextcn  23982  minveclem4a  25357  oldf  27798  madefi  27858  precsexlem10  28154  xrge0tsmsbi  33043  dimval  33613  dimvalfi  33614  locfinreflem  33853  pstmfval  33909  pstmxmet  33910  esumex  34042  msrval  35582  dfrdg2  35837  fvbigcup  35944  ctbssinf  37450  ptrest  37658  heiborlem1  37850  heiborlem3  37852  heibor  37860  dicval  41274  prjcrvfval  42723  aomclem1  43146  dfac21  43158  ntrrn  44214  ntrf  44215  dssmapntrcls  44220  permaxun  45103  fourierdlem70  46273  caragendifcl  46611  cnfsmf  46837  tposideq  48987  setrec1lem3  49789  setrec2fun  49792