Theorem uniex 7698

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442  ∪ cuni 4865

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 5245  ax-un 7692

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 3444  df-ss 3920  df-uni 4866

This theorem is referenced by:  unexOLD  7702  iunpw  7728  elxp4  7876  elxp5  7877  1stval  7947  2ndval  7948  fo1st  7965  fo2nd  7966  cnvf1o  8065  brtpos2  8186  naddcllem  8616  ixpsnf1o  8890  dffi3  9348  cnfcom2  9625  cnfcom3lem  9626  cnfcom3  9627  ttrclse  9650  trcl  9651  rankc2  9797  rankxpl  9801  rankxpsuc  9808  acnlem  9972  dfac2a  10054  fin23lem14  10257  fin23lem16  10259  fin23lem17  10262  fin23lem38  10273  fin23lem39  10274  itunisuc  10343  axdc3lem2  10375  axcclem  10381  ac5b  10402  ttukey  10442  wunex2  10663  wuncval2  10672  intgru  10739  pnfex  11199  prdsvallem  17388  prdsval  17389  prdsds  17398  wunfunc  17839  wunnat  17897  arwval  17981  catcfuccl  18056  catcxpccl  18144  zrhval  21479  mreclatdemoBAD  23057  ptbasin2  23539  ptbasfi  23542  dfac14  23579  ptcmplem2  24014  ptcmplem3  24015  ptcmp  24019  cnextfvval  24026  cnextcn  24028  minveclem4a  25403  oldf  27850  madefi  27926  precsexlem10  28229  xrge0tsmsbi  33174  dimval  33784  dimvalfi  33785  locfinreflem  34024  pstmfval  34080  pstmxmet  34081  esumex  34213  msrval  35760  dfrdg2  36015  fvbigcup  36122  ctbssinf  37688  ptrest  37899  heiborlem1  38091  heiborlem3  38093  heibor  38101  dicval  41581  prjcrvfval  43018  aomclem1  43440  dfac21  43452  ntrrn  44507  ntrf  44508  dssmapntrcls  44513  permaxun  45396  fourierdlem70  46563  caragendifcl  46901  cnfsmf  47127  tposideq  49276  setrec1lem3  50077  setrec2fun  50080