Theorem uniex 7720

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450  ∪ cuni 4874

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 2702  ax-sep 5254  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-uni 4875

This theorem is referenced by:  unexOLD  7724  iunpw  7750  elxp4  7901  elxp5  7902  1stval  7973  2ndval  7974  fo1st  7991  fo2nd  7992  cnvf1o  8093  brtpos2  8214  naddcllem  8643  ixpsnf1o  8914  dffi3  9389  cnfcom2  9662  cnfcom3lem  9663  cnfcom3  9664  ttrclse  9687  trcl  9688  rankc2  9831  rankxpl  9835  rankxpsuc  9842  acnlem  10008  dfac2a  10090  fin23lem14  10293  fin23lem16  10295  fin23lem17  10298  fin23lem38  10309  fin23lem39  10310  itunisuc  10379  axdc3lem2  10411  axcclem  10417  ac5b  10438  ttukey  10478  wunex2  10698  wuncval2  10707  intgru  10774  pnfex  11234  prdsvallem  17424  prdsval  17425  prdsds  17434  wunfunc  17870  wunnat  17928  arwval  18012  catcfuccl  18087  catcxpccl  18175  zrhval  21424  mreclatdemoBAD  22990  ptbasin2  23472  ptbasfi  23475  dfac14  23512  ptcmplem2  23947  ptcmplem3  23948  ptcmp  23952  cnextfvval  23959  cnextcn  23961  minveclem4a  25337  oldf  27772  madefi  27831  precsexlem10  28125  xrge0tsmsbi  33010  dimval  33603  dimvalfi  33604  locfinreflem  33837  pstmfval  33893  pstmxmet  33894  esumex  34026  msrval  35532  dfrdg2  35790  fvbigcup  35897  ctbssinf  37401  ptrest  37620  heiborlem1  37812  heiborlem3  37814  heibor  37822  dicval  41177  prjcrvfval  42626  aomclem1  43050  dfac21  43062  ntrrn  44118  ntrf  44119  dssmapntrcls  44124  permaxun  45008  fourierdlem70  46181  caragendifcl  46519  cnfsmf  46745  tposideq  48880  setrec1lem3  49682  setrec2fun  49685