Theorem uniex 7746

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3453  ∪ cuni 4870

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-un 7739

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-uni 4871

This theorem is used by:  iunpw  7773  elxp4  7922  elxp5  7923  1stval  7991  2ndval  7992  fo1st  8009  fo2nd  8010  cnvf1o  8111  brtpos2  8233  naddcllem  8667  ixpsnf1o  8948  dffi3  9404  cnfcom2  9684  cnfcom3lem  9685  cnfcom3  9686  ttrclse  9709  trcl  9710  rankc2  9856  rankxpl  9860  rankxpsuc  9867  acnlem  10054  dfac2a  10135  fin23lem14  10338  fin23lem16  10340  fin23lem17  10343  fin23lem38  10354  fin23lem39  10355  itunisuc  10424  axdc3lem2  10456  axcclem  10462  ac5b  10483  ttukey  10523  wunex2  10750  wuncval2  10759  intgru  10826  pnfex  11289  prdsvallem  17543  prdsval  17544  prdsds  17553  wunfunc  17994  wunnat  18052  arwval  18136  catcfuccl  18211  catcxpccl  18299  zrhval  21721  mreclatdemoBAD  23322  ptbasin2  23805  ptbasfi  23808  dfac14  23845  ptcmplem2  24280  ptcmplem3  24281  ptcmp  24285  cnextfvval  24292  cnextcn  24294  minveclem4a  25659  oldf  28100  precsexlem10  28479  xrge0tsmsbi  33501  dimval  34098  dimvalfi  34099  locfinreflem  34337  pstmfval  34393  pstmxmet  34394  esumex  34526  msrval  36104  dfrdg2  36359  fvbigcup  36466  ttctr  37099  ttcmin  37102  dfttc2g  37112  ctbssinf  38147  ptrest  38355  heiborlem1  38548  heiborlem3  38550  heibor  38558  dicval  42036  prjcrvfval  43464  aomclem1  43882  dfac21  43894  ntrrn  44949  ntrf  44950  dssmapntrcls  44955  permaxun  45821  fourierdlem70  46991  caragendifcl  47329  cnfsmf  47555  tposideq  49801  setrec1lem3  50602  setrec2fun  50605