Theorem uniex 7731

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475  ∪ cuni 4909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910

This theorem is referenced by:  unex  7733  iunpw  7758  elxp4  7913  elxp5  7914  1stval  7977  2ndval  7978  fo1st  7995  fo2nd  7996  cnvf1o  8097  brtpos2  8217  naddcllem  8675  ixpsnf1o  8932  dffi3  9426  cnfcom2  9697  cnfcom3lem  9698  cnfcom3  9699  ttrclse  9722  trcl  9723  rankc2  9866  rankxpl  9870  rankxpsuc  9877  acnlem  10043  dfac2a  10124  fin23lem14  10328  fin23lem16  10330  fin23lem17  10333  fin23lem38  10344  fin23lem39  10345  itunisuc  10414  axdc3lem2  10446  axcclem  10452  ac5b  10473  ttukey  10513  wunex2  10733  wuncval2  10742  intgru  10809  pnfex  11267  prdsvallem  17400  prdsval  17401  prdsds  17410  wunfunc  17849  wunfuncOLD  17850  wunnat  17907  wunnatOLD  17908  arwval  17993  catcfuccl  18069  catcfucclOLD  18070  catcxpccl  18159  catcxpcclOLD  18160  zrhval  21057  mreclatdemoBAD  22600  ptbasin2  23082  ptbasfi  23085  dfac14  23122  ptcmplem2  23557  ptcmplem3  23558  ptcmp  23562  cnextfvval  23569  cnextcn  23571  minveclem4a  24947  oldf  27352  precsexlem10  27662  xrge0tsmsbi  32210  dimval  32686  dimvalfi  32687  locfinreflem  32820  pstmfval  32876  pstmxmet  32877  esumex  33027  msrval  34529  dfrdg2  34767  fvbigcup  34874  ctbssinf  36287  ptrest  36487  heiborlem1  36679  heiborlem3  36681  heibor  36689  dicval  40047  prjcrvfval  41373  aomclem1  41796  dfac21  41808  ntrrn  42873  ntrf  42874  dssmapntrcls  42879  fourierdlem70  44892  caragendifcl  45230  cnfsmf  45456  setrec1lem3  47734  setrec2fun  47737