Theorem uniex 7684

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

Syntax hints:   ∈ wcel 2114  Vcvv 3427  ∪ cuni 4840

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 5220  ax-un 7678

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 3429  df-ss 3902  df-uni 4841

This theorem is referenced by:  unexOLD  7688  iunpw  7714  elxp4  7862  elxp5  7863  1stval  7933  2ndval  7934  fo1st  7951  fo2nd  7952  cnvf1o  8050  brtpos2  8171  naddcllem  8601  ixpsnf1o  8875  dffi3  9333  cnfcom2  9612  cnfcom3lem  9613  cnfcom3  9614  ttrclse  9637  trcl  9638  rankc2  9784  rankxpl  9788  rankxpsuc  9795  acnlem  9959  dfac2a  10041  fin23lem14  10244  fin23lem16  10246  fin23lem17  10249  fin23lem38  10260  fin23lem39  10261  itunisuc  10330  axdc3lem2  10362  axcclem  10368  ac5b  10389  ttukey  10429  wunex2  10650  wuncval2  10659  intgru  10726  pnfex  11187  prdsvallem  17406  prdsval  17407  prdsds  17416  wunfunc  17857  wunnat  17915  arwval  17999  catcfuccl  18074  catcxpccl  18162  zrhval  21476  mreclatdemoBAD  23049  ptbasin2  23531  ptbasfi  23534  dfac14  23571  ptcmplem2  24006  ptcmplem3  24007  ptcmp  24011  cnextfvval  24018  cnextcn  24020  minveclem4a  25385  oldf  27817  madefi  27893  precsexlem10  28196  xrge0tsmsbi  33123  dimval  33733  dimvalfi  33734  locfinreflem  33972  pstmfval  34028  pstmxmet  34029  esumex  34161  msrval  35708  dfrdg2  35963  fvbigcup  36070  ttctr  36663  ttcmin  36666  dfttc2g  36676  ctbssinf  37710  ptrest  37928  heiborlem1  38120  heiborlem3  38122  heibor  38130  dicval  41610  prjcrvfval  43052  aomclem1  43470  dfac21  43482  ntrrn  44537  ntrf  44538  dssmapntrcls  44543  permaxun  45426  fourierdlem70  46592  caragendifcl  46930  cnfsmf  47156  tposideq  49351  setrec1lem3  50152  setrec2fun  50155