Theorem uniex 7447

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

Syntax hints:   ∈ wcel 2111  Vcvv 3441  ∪ cuni 4800

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-sep 5167  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801

This theorem is referenced by:  unex  7449  iunpw  7473  elxp4  7609  elxp5  7610  1stval  7673  2ndval  7674  fo1st  7691  fo2nd  7692  cnvf1o  7789  brtpos2  7881  ixpsnf1o  8485  dffi3  8879  cnfcom2  9149  cnfcom3lem  9150  cnfcom3  9151  trcl  9154  rankc2  9284  rankxpl  9288  rankxpsuc  9295  acnlem  9459  dfac2a  9540  fin23lem14  9744  fin23lem16  9746  fin23lem17  9749  fin23lem38  9760  fin23lem39  9761  itunisuc  9830  axdc3lem2  9862  axcclem  9868  ac5b  9889  ttukey  9929  wunex2  10149  wuncval2  10158  intgru  10225  pnfex  10683  prdsval  16720  prdsds  16729  wunfunc  17161  wunnat  17218  arwval  17295  catcfuccl  17361  catcxpccl  17449  zrhval  20201  mreclatdemoBAD  21701  ptbasin2  22183  ptbasfi  22186  dfac14  22223  ptcmplem2  22658  ptcmplem3  22659  ptcmp  22663  cnextfvval  22670  cnextcn  22672  minveclem4a  24034  xrge0tsmsbi  30743  dimval  31089  dimvalfi  31090  locfinreflem  31193  pstmfval  31249  pstmxmet  31250  esumex  31398  msrval  32898  dfrdg2  33153  trpredex  33189  fvbigcup  33476  ctbssinf  34823  ptrest  35056  heiborlem1  35249  heiborlem3  35251  heibor  35259  dicval  38472  aomclem1  39998  dfac21  40010  ntrrn  40825  ntrf  40826  dssmapntrcls  40831  fourierdlem70  42818  caragendifcl  43153  cnfsmf  43374  setrec1lem3  45219  setrec2fun  45222