Theorem uniex 7469

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

Syntax hints:   ∈ wcel 2114  Vcvv 3496  ∪ cuni 4840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954  df-uni 4841

This theorem is referenced by:  unex  7471  iunpw  7495  elxp4  7629  elxp5  7630  1stval  7693  2ndval  7694  fo1st  7711  fo2nd  7712  cnvf1o  7808  brtpos2  7900  ixpsnf1o  8504  dffi3  8897  cnfcom2  9167  cnfcom3lem  9168  cnfcom3  9169  trcl  9172  rankc2  9302  rankxpl  9306  rankxpsuc  9313  acnlem  9476  dfac2a  9557  fin23lem14  9757  fin23lem16  9759  fin23lem17  9762  fin23lem38  9773  fin23lem39  9774  itunisuc  9843  axdc3lem2  9875  axcclem  9881  ac5b  9902  ttukey  9942  wunex2  10162  wuncval2  10171  intgru  10238  pnfex  10696  prdsval  16730  prdsds  16739  wunfunc  17171  wunnat  17228  arwval  17305  catcfuccl  17371  catcxpccl  17459  zrhval  20657  mreclatdemoBAD  21706  ptbasin2  22188  ptbasfi  22191  dfac14  22228  ptcmplem2  22663  ptcmplem3  22664  ptcmp  22668  cnextfvval  22675  cnextcn  22677  minveclem4a  24035  xrge0tsmsbi  30695  dimval  31003  dimvalfi  31004  locfinreflem  31106  pstmfval  31138  pstmxmet  31139  esumex  31290  msrval  32787  dfrdg2  33042  trpredex  33078  fvbigcup  33365  ctbssinf  34689  ptrest  34893  heiborlem1  35091  heiborlem3  35093  heibor  35101  dicval  38314  aomclem1  39661  dfac21  39673  ntrrn  40479  ntrf  40480  dssmapntrcls  40485  fourierdlem70  42468  caragendifcl  42803  cnfsmf  43024  setrec1lem3  44799  setrec2fun  44802