Theorem uniex 7727

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

Syntax hints:   ∈ wcel 2106  Vcvv 3474  ∪ cuni 4907

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-uni 4908

This theorem is referenced by:  unex  7729  iunpw  7754  elxp4  7909  elxp5  7910  1stval  7973  2ndval  7974  fo1st  7991  fo2nd  7992  cnvf1o  8093  brtpos2  8213  naddcllem  8671  ixpsnf1o  8928  dffi3  9422  cnfcom2  9693  cnfcom3lem  9694  cnfcom3  9695  ttrclse  9718  trcl  9719  rankc2  9862  rankxpl  9866  rankxpsuc  9873  acnlem  10039  dfac2a  10120  fin23lem14  10324  fin23lem16  10326  fin23lem17  10329  fin23lem38  10340  fin23lem39  10341  itunisuc  10410  axdc3lem2  10442  axcclem  10448  ac5b  10469  ttukey  10509  wunex2  10729  wuncval2  10738  intgru  10805  pnfex  11263  prdsvallem  17396  prdsval  17397  prdsds  17406  wunfunc  17845  wunfuncOLD  17846  wunnat  17903  wunnatOLD  17904  arwval  17989  catcfuccl  18065  catcfucclOLD  18066  catcxpccl  18155  catcxpcclOLD  18156  zrhval  21048  mreclatdemoBAD  22591  ptbasin2  23073  ptbasfi  23076  dfac14  23113  ptcmplem2  23548  ptcmplem3  23549  ptcmp  23553  cnextfvval  23560  cnextcn  23562  minveclem4a  24938  oldf  27341  precsexlem10  27651  xrge0tsmsbi  32197  dimval  32674  dimvalfi  32675  locfinreflem  32808  pstmfval  32864  pstmxmet  32865  esumex  33015  msrval  34517  dfrdg2  34755  fvbigcup  34862  ctbssinf  36275  ptrest  36475  heiborlem1  36667  heiborlem3  36669  heibor  36677  dicval  40035  prjcrvfval  41369  aomclem1  41781  dfac21  41793  ntrrn  42858  ntrf  42859  dssmapntrcls  42864  fourierdlem70  44878  caragendifcl  45216  cnfsmf  45442  setrec1lem3  47687  setrec2fun  47690