Theorem uniex 7746

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

Syntax hints:   ∈ wcel 2099  Vcvv 3471  ∪ cuni 4908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-sep 5299  ax-un 7740

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-in 3954  df-ss 3964  df-uni 4909

This theorem is referenced by:  unex  7748  iunpw  7773  elxp4  7930  elxp5  7931  1stval  7995  2ndval  7996  fo1st  8013  fo2nd  8014  cnvf1o  8116  brtpos2  8238  naddcllem  8697  ixpsnf1o  8957  dffi3  9455  cnfcom2  9726  cnfcom3lem  9727  cnfcom3  9728  ttrclse  9751  trcl  9752  rankc2  9895  rankxpl  9899  rankxpsuc  9906  acnlem  10072  dfac2a  10153  fin23lem14  10357  fin23lem16  10359  fin23lem17  10362  fin23lem38  10373  fin23lem39  10374  itunisuc  10443  axdc3lem2  10475  axcclem  10481  ac5b  10502  ttukey  10542  wunex2  10762  wuncval2  10771  intgru  10838  pnfex  11298  prdsvallem  17436  prdsval  17437  prdsds  17446  wunfunc  17887  wunfuncOLD  17888  wunnat  17946  wunnatOLD  17947  arwval  18032  catcfuccl  18108  catcfucclOLD  18109  catcxpccl  18198  catcxpcclOLD  18199  zrhval  21433  mreclatdemoBAD  23013  ptbasin2  23495  ptbasfi  23498  dfac14  23535  ptcmplem2  23970  ptcmplem3  23971  ptcmp  23975  cnextfvval  23982  cnextcn  23984  minveclem4a  25371  oldf  27797  precsexlem10  28127  xrge0tsmsbi  32785  dimval  33298  dimvalfi  33299  locfinreflem  33441  pstmfval  33497  pstmxmet  33498  esumex  33648  msrval  35148  dfrdg2  35391  fvbigcup  35498  ctbssinf  36885  ptrest  37092  heiborlem1  37284  heiborlem3  37286  heibor  37294  dicval  40649  prjcrvfval  42055  aomclem1  42478  dfac21  42490  ntrrn  43552  ntrf  43553  dssmapntrcls  43558  fourierdlem70  45564  caragendifcl  45902  cnfsmf  46128  setrec1lem3  48120  setrec2fun  48123