Theorem uniex 7695

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  ∪ cuni 4851

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 2709  ax-sep 5232  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-uni 4852

This theorem is referenced by:  unexOLD  7699  iunpw  7725  elxp4  7873  elxp5  7874  1stval  7944  2ndval  7945  fo1st  7962  fo2nd  7963  cnvf1o  8061  brtpos2  8182  naddcllem  8612  ixpsnf1o  8886  dffi3  9344  cnfcom2  9623  cnfcom3lem  9624  cnfcom3  9625  ttrclse  9648  trcl  9649  rankc2  9795  rankxpl  9799  rankxpsuc  9806  acnlem  9970  dfac2a  10052  fin23lem14  10255  fin23lem16  10257  fin23lem17  10260  fin23lem38  10271  fin23lem39  10272  itunisuc  10341  axdc3lem2  10373  axcclem  10379  ac5b  10400  ttukey  10440  wunex2  10661  wuncval2  10670  intgru  10737  pnfex  11198  prdsvallem  17417  prdsval  17418  prdsds  17427  wunfunc  17868  wunnat  17926  arwval  18010  catcfuccl  18085  catcxpccl  18173  zrhval  21487  mreclatdemoBAD  23061  ptbasin2  23543  ptbasfi  23546  dfac14  23583  ptcmplem2  24018  ptcmplem3  24019  ptcmp  24023  cnextfvval  24030  cnextcn  24032  minveclem4a  25397  oldf  27829  madefi  27905  precsexlem10  28208  xrge0tsmsbi  33135  dimval  33745  dimvalfi  33746  locfinreflem  33984  pstmfval  34040  pstmxmet  34041  esumex  34173  msrval  35720  dfrdg2  35975  fvbigcup  36082  ttctr  36675  ttcmin  36678  dfttc2g  36688  ctbssinf  37722  ptrest  37940  heiborlem1  38132  heiborlem3  38134  heibor  38142  dicval  41622  prjcrvfval  43064  aomclem1  43482  dfac21  43494  ntrrn  44549  ntrf  44550  dssmapntrcls  44555  permaxun  45438  fourierdlem70  46604  caragendifcl  46942  cnfsmf  47168  tposideq  49357  setrec1lem3  50158  setrec2fun  50161