Theorem uniex 7686

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

Syntax hints:   ∈ wcel 2114  Vcvv 3439  ∪ cuni 4862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5240  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3441  df-ss 3917  df-uni 4863

This theorem is referenced by:  unexOLD  7690  iunpw  7716  elxp4  7864  elxp5  7865  1stval  7935  2ndval  7936  fo1st  7953  fo2nd  7954  cnvf1o  8053  brtpos2  8174  naddcllem  8604  ixpsnf1o  8878  dffi3  9336  cnfcom2  9613  cnfcom3lem  9614  cnfcom3  9615  ttrclse  9638  trcl  9639  rankc2  9785  rankxpl  9789  rankxpsuc  9796  acnlem  9960  dfac2a  10042  fin23lem14  10245  fin23lem16  10247  fin23lem17  10250  fin23lem38  10261  fin23lem39  10262  itunisuc  10331  axdc3lem2  10363  axcclem  10369  ac5b  10390  ttukey  10430  wunex2  10651  wuncval2  10660  intgru  10727  pnfex  11187  prdsvallem  17376  prdsval  17377  prdsds  17386  wunfunc  17827  wunnat  17885  arwval  17969  catcfuccl  18044  catcxpccl  18132  zrhval  21464  mreclatdemoBAD  23042  ptbasin2  23524  ptbasfi  23527  dfac14  23564  ptcmplem2  23999  ptcmplem3  24000  ptcmp  24004  cnextfvval  24011  cnextcn  24013  minveclem4a  25388  oldf  27833  madefi  27893  precsexlem10  28195  xrge0tsmsbi  33135  dimval  33736  dimvalfi  33737  locfinreflem  33976  pstmfval  34032  pstmxmet  34033  esumex  34165  msrval  35711  dfrdg2  35966  fvbigcup  36073  ctbssinf  37580  ptrest  37789  heiborlem1  37981  heiborlem3  37983  heibor  37991  dicval  41471  prjcrvfval  42911  aomclem1  43333  dfac21  43345  ntrrn  44400  ntrf  44401  dssmapntrcls  44406  permaxun  45289  fourierdlem70  46457  caragendifcl  46795  cnfsmf  47021  tposideq  49170  setrec1lem3  49971  setrec2fun  49974