Theorem uniex 7739

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

Syntax hints:   ∈ wcel 2141  Vcvv 3453  ∪ cuni 4871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5256  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3921  df-uni 4872

This theorem is referenced by:  unexOLD  7743  iunpw  7769  elxp4  7918  elxp5  7919  1stval  7987  2ndval  7988  fo1st  8005  fo2nd  8006  cnvf1o  8105  brtpos2  8227  naddcllem  8661  ixpsnf1o  8935  dffi3  9390  cnfcom2  9670  cnfcom3lem  9671  cnfcom3  9672  ttrclse  9695  trcl  9696  rankc2  9842  rankxpl  9846  rankxpsuc  9853  acnlem  10031  dfac2a  10112  fin23lem14  10316  fin23lem16  10318  fin23lem17  10321  fin23lem38  10332  fin23lem39  10333  itunisuc  10402  axdc3lem2  10434  axcclem  10440  ac5b  10461  ttukey  10501  wunex2  10722  wuncval2  10731  intgru  10798  pnfex  11261  prdsvallem  17506  prdsval  17507  prdsds  17516  wunfunc  17957  wunnat  18015  arwval  18099  catcfuccl  18174  catcxpccl  18262  zrhval  21636  mreclatdemoBAD  23232  ptbasin2  23714  ptbasfi  23717  dfac14  23754  ptcmplem2  24189  ptcmplem3  24190  ptcmp  24194  cnextfvval  24201  cnextcn  24203  minveclem4a  25568  oldf  28006  madefi  28082  precsexlem10  28385  xrge0tsmsbi  33360  dimval  33957  dimvalfi  33958  locfinreflem  34196  pstmfval  34252  pstmxmet  34253  esumex  34385  msrval  35984  dfrdg2  36239  fvbigcup  36346  ttctr  36948  ttcmin  36951  dfttc2g  36961  ctbssinf  37996  ptrest  38214  heiborlem1  38406  heiborlem3  38408  heibor  38416  dicval  41896  prjcrvfval  43311  aomclem1  43729  dfac21  43741  ntrrn  44796  ntrf  44797  dssmapntrcls  44802  permaxun  45668  fourierdlem70  46838  caragendifcl  47176  cnfsmf  47402  tposideq  49611  setrec1lem3  50412  setrec2fun  50415