Theorem uniex 7459

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

Syntax hints:   ∈ wcel 2108  Vcvv 3493  ∪ cuni 4830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-un 7453

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rex 3142  df-v 3495  df-uni 4831

This theorem is referenced by:  unex  7461  iunpw  7485  elxp4  7619  elxp5  7620  1stval  7683  2ndval  7684  fo1st  7701  fo2nd  7702  cnvf1o  7798  brtpos2  7890  ixpsnf1o  8494  dffi3  8887  cnfcom2  9157  cnfcom3lem  9158  cnfcom3  9159  trcl  9162  rankc2  9292  rankxpl  9296  rankxpsuc  9303  acnlem  9466  dfac2a  9547  fin23lem14  9747  fin23lem16  9749  fin23lem17  9752  fin23lem38  9763  fin23lem39  9764  itunisuc  9833  axdc3lem2  9865  axcclem  9871  ac5b  9892  ttukey  9932  wunex2  10152  wuncval2  10161  intgru  10228  pnfex  10686  prdsval  16720  prdsds  16729  wunfunc  17161  wunnat  17218  arwval  17295  catcfuccl  17361  catcxpccl  17449  zrhval  20647  mreclatdemoBAD  21696  ptbasin2  22178  ptbasfi  22181  dfac14  22218  ptcmplem2  22653  ptcmplem3  22654  ptcmp  22658  cnextfvval  22665  cnextcn  22667  minveclem4a  24025  xrge0tsmsbi  30686  dimval  30994  dimvalfi  30995  locfinreflem  31097  pstmfval  31129  pstmxmet  31130  esumex  31281  msrval  32778  dfrdg2  33033  trpredex  33069  fvbigcup  33356  ctbssinf  34679  ptrest  34883  heiborlem1  35081  heiborlem3  35083  heibor  35091  dicval  38304  aomclem1  39644  dfac21  39656  ntrrn  40462  ntrf  40463  dssmapntrcls  40468  fourierdlem70  42451  caragendifcl  42786  cnfsmf  43007  setrec1lem3  44782  setrec2fun  44785