Theorem uniex 7572

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

Syntax hints:   ∈ wcel 2108  Vcvv 3422  ∪ cuni 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837

This theorem is referenced by:  unex  7574  iunpw  7599  elxp4  7743  elxp5  7744  1stval  7806  2ndval  7807  fo1st  7824  fo2nd  7825  cnvf1o  7922  brtpos2  8019  ixpsnf1o  8684  dffi3  9120  cnfcom2  9390  cnfcom3lem  9391  cnfcom3  9392  trpredex  9416  trcl  9417  rankc2  9560  rankxpl  9564  rankxpsuc  9571  acnlem  9735  dfac2a  9816  fin23lem14  10020  fin23lem16  10022  fin23lem17  10025  fin23lem38  10036  fin23lem39  10037  itunisuc  10106  axdc3lem2  10138  axcclem  10144  ac5b  10165  ttukey  10205  wunex2  10425  wuncval2  10434  intgru  10501  pnfex  10959  prdsvallem  17082  prdsval  17083  prdsds  17092  wunfunc  17530  wunfuncOLD  17531  wunnat  17588  wunnatOLD  17589  arwval  17674  catcfuccl  17750  catcfucclOLD  17751  catcxpccl  17840  catcxpcclOLD  17841  zrhval  20621  mreclatdemoBAD  22155  ptbasin2  22637  ptbasfi  22640  dfac14  22677  ptcmplem2  23112  ptcmplem3  23113  ptcmp  23117  cnextfvval  23124  cnextcn  23126  minveclem4a  24499  xrge0tsmsbi  31220  dimval  31588  dimvalfi  31589  locfinreflem  31692  pstmfval  31748  pstmxmet  31749  esumex  31897  msrval  33400  dfrdg2  33677  ttrclse  33713  naddcllem  33758  oldf  33968  fvbigcup  34131  ctbssinf  35504  ptrest  35703  heiborlem1  35896  heiborlem3  35898  heibor  35906  dicval  39117  aomclem1  40795  dfac21  40807  ntrrn  41621  ntrf  41622  dssmapntrcls  41627  fourierdlem70  43607  caragendifcl  43942  cnfsmf  44163  setrec1lem3  46281  setrec2fun  46284