Theorem uniex 7687

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

Syntax hints:   ∈ wcel 2121  Vcvv 3433  ∪ cuni 4840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5220  ax-un 7681

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3901  df-uni 4841

This theorem is referenced by:  unexOLD  7691  iunpw  7717  elxp4  7866  elxp5  7867  1stval  7935  2ndval  7936  fo1st  7953  fo2nd  7954  cnvf1o  8052  brtpos2  8174  naddcllem  8606  ixpsnf1o  8880  dffi3  9338  cnfcom2  9618  cnfcom3lem  9619  cnfcom3  9620  ttrclse  9643  trcl  9644  rankc2  9790  rankxpl  9794  rankxpsuc  9801  acnlem  9965  dfac2a  10047  fin23lem14  10251  fin23lem16  10253  fin23lem17  10256  fin23lem38  10267  fin23lem39  10268  itunisuc  10337  axdc3lem2  10369  axcclem  10375  ac5b  10396  ttukey  10436  wunex2  10657  wuncval2  10666  intgru  10733  pnfex  11194  prdsvallem  17412  prdsval  17413  prdsds  17422  wunfunc  17863  wunnat  17921  arwval  18005  catcfuccl  18080  catcxpccl  18168  zrhval  21485  mreclatdemoBAD  23082  ptbasin2  23564  ptbasfi  23567  dfac14  23604  ptcmplem2  24039  ptcmplem3  24040  ptcmp  24044  cnextfvval  24051  cnextcn  24053  minveclem4a  25418  oldf  27849  madefi  27925  precsexlem10  28228  xrge0tsmsbi  33157  dimval  33795  dimvalfi  33796  locfinreflem  34034  pstmfval  34090  pstmxmet  34091  esumex  34223  msrval  35779  dfrdg2  36034  fvbigcup  36141  ttctr  36734  ttcmin  36737  dfttc2g  36747  ctbssinf  37781  ptrest  37999  heiborlem1  38191  heiborlem3  38193  heibor  38201  dicval  41681  prjcrvfval  43094  aomclem1  43512  dfac21  43524  ntrrn  44579  ntrf  44580  dssmapntrcls  44585  permaxun  45468  fourierdlem70  46631  caragendifcl  46969  cnfsmf  47195  tposideq  49390  setrec1lem3  50191  setrec2fun  50194