Theorem uniex 7726

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

Syntax hints:   ∈ wcel 2144  Vcvv 3456  ∪ cuni 4867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-un 7720

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-ss 3923  df-uni 4868

This theorem is referenced by:  unexOLD  7730  iunpw  7756  elxp4  7905  elxp5  7906  1stval  7974  2ndval  7975  fo1st  7992  fo2nd  7993  cnvf1o  8092  brtpos2  8214  naddcllem  8648  ixpsnf1o  8922  dffi3  9379  cnfcom2  9659  cnfcom3lem  9660  cnfcom3  9661  ttrclse  9684  trcl  9685  rankc2  9831  rankxpl  9835  rankxpsuc  9842  acnlem  10006  dfac2a  10088  fin23lem14  10292  fin23lem16  10294  fin23lem17  10297  fin23lem38  10308  fin23lem39  10309  itunisuc  10378  axdc3lem2  10410  axcclem  10416  ac5b  10437  ttukey  10477  wunex2  10698  wuncval2  10707  intgru  10774  pnfex  11237  prdsvallem  17485  prdsval  17486  prdsds  17495  wunfunc  17936  wunnat  17994  arwval  18078  catcfuccl  18153  catcxpccl  18241  zrhval  21561  mreclatdemoBAD  23158  ptbasin2  23640  ptbasfi  23643  dfac14  23680  ptcmplem2  24115  ptcmplem3  24116  ptcmp  24120  cnextfvval  24127  cnextcn  24129  minveclem4a  25494  oldf  27932  madefi  28008  precsexlem10  28311  xrge0tsmsbi  33256  dimval  33900  dimvalfi  33901  locfinreflem  34139  pstmfval  34195  pstmxmet  34196  esumex  34328  msrval  35893  dfrdg2  36148  fvbigcup  36255  ttctr  36858  ttcmin  36861  dfttc2g  36871  ctbssinf  37905  ptrest  38123  heiborlem1  38315  heiborlem3  38317  heibor  38325  dicval  41805  prjcrvfval  43218  aomclem1  43636  dfac21  43648  ntrrn  44703  ntrf  44704  dssmapntrcls  44709  permaxun  45592  fourierdlem70  46755  caragendifcl  47093  cnfsmf  47319  tposideq  49514  setrec1lem3  50315  setrec2fun  50318