Theorem uniex 7760

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

Syntax hints:   ∈ wcel 2106  Vcvv 3478  ∪ cuni 4912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-uni 4913

This theorem is referenced by:  unexOLD  7764  iunpw  7790  elxp4  7945  elxp5  7946  1stval  8015  2ndval  8016  fo1st  8033  fo2nd  8034  cnvf1o  8135  brtpos2  8256  naddcllem  8713  ixpsnf1o  8977  dffi3  9469  cnfcom2  9740  cnfcom3lem  9741  cnfcom3  9742  ttrclse  9765  trcl  9766  rankc2  9909  rankxpl  9913  rankxpsuc  9920  acnlem  10086  dfac2a  10168  fin23lem14  10371  fin23lem16  10373  fin23lem17  10376  fin23lem38  10387  fin23lem39  10388  itunisuc  10457  axdc3lem2  10489  axcclem  10495  ac5b  10516  ttukey  10556  wunex2  10776  wuncval2  10785  intgru  10852  pnfex  11312  prdsvallem  17501  prdsval  17502  prdsds  17511  wunfunc  17952  wunfuncOLD  17953  wunnat  18011  wunnatOLD  18012  arwval  18097  catcfuccl  18173  catcfucclOLD  18174  catcxpccl  18263  catcxpcclOLD  18264  zrhval  21536  mreclatdemoBAD  23120  ptbasin2  23602  ptbasfi  23605  dfac14  23642  ptcmplem2  24077  ptcmplem3  24078  ptcmp  24082  cnextfvval  24089  cnextcn  24091  minveclem4a  25478  oldf  27911  madefi  27965  precsexlem10  28255  xrge0tsmsbi  33049  dimval  33628  dimvalfi  33629  locfinreflem  33801  pstmfval  33857  pstmxmet  33858  esumex  34010  msrval  35523  dfrdg2  35777  fvbigcup  35884  ctbssinf  37389  ptrest  37606  heiborlem1  37798  heiborlem3  37800  heibor  37808  dicval  41159  prjcrvfval  42618  aomclem1  43043  dfac21  43055  ntrrn  44112  ntrf  44113  dssmapntrcls  44118  fourierdlem70  46132  caragendifcl  46470  cnfsmf  46696  setrec1lem3  48920  setrec2fun  48923