Theorem uniex 7697

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

Syntax hints:   ∈ wcel 2109  Vcvv 3444  ∪ cuni 4867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-uni 4868

This theorem is referenced by:  unexOLD  7701  iunpw  7727  elxp4  7878  elxp5  7879  1stval  7949  2ndval  7950  fo1st  7967  fo2nd  7968  cnvf1o  8067  brtpos2  8188  naddcllem  8617  ixpsnf1o  8888  dffi3  9358  cnfcom2  9631  cnfcom3lem  9632  cnfcom3  9633  ttrclse  9656  trcl  9657  rankc2  9800  rankxpl  9804  rankxpsuc  9811  acnlem  9977  dfac2a  10059  fin23lem14  10262  fin23lem16  10264  fin23lem17  10267  fin23lem38  10278  fin23lem39  10279  itunisuc  10348  axdc3lem2  10380  axcclem  10386  ac5b  10407  ttukey  10447  wunex2  10667  wuncval2  10676  intgru  10743  pnfex  11203  prdsvallem  17393  prdsval  17394  prdsds  17403  wunfunc  17843  wunnat  17901  arwval  17985  catcfuccl  18060  catcxpccl  18148  zrhval  21449  mreclatdemoBAD  23016  ptbasin2  23498  ptbasfi  23501  dfac14  23538  ptcmplem2  23973  ptcmplem3  23974  ptcmp  23978  cnextfvval  23985  cnextcn  23987  minveclem4a  25363  oldf  27802  madefi  27862  precsexlem10  28158  xrge0tsmsbi  33046  dimval  33589  dimvalfi  33590  locfinreflem  33823  pstmfval  33879  pstmxmet  33880  esumex  34012  msrval  35518  dfrdg2  35776  fvbigcup  35883  ctbssinf  37387  ptrest  37606  heiborlem1  37798  heiborlem3  37800  heibor  37808  dicval  41163  prjcrvfval  42612  aomclem1  43036  dfac21  43048  ntrrn  44104  ntrf  44105  dssmapntrcls  44110  permaxun  44994  fourierdlem70  46167  caragendifcl  46505  cnfsmf  46731  tposideq  48869  setrec1lem3  49671  setrec2fun  49674