Theorem uniex 7758

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-uni 4867

This theorem is used by:  iunpw  7785  elxp4  7934  elxp5  7935  1stval  8003  2ndval  8004  fo1st  8021  fo2nd  8022  cnvf1o  8122  brtpos2  8249  naddcllem  8685  ixpsnf1o  8966  dffi3  9423  cnfcom2  9703  cnfcom3lem  9704  cnfcom3  9705  ttrclse  9728  trcl  9729  rankc2  9888  rankxpl  9892  rankxpsuc  9899  setrec1lem3  9969  setrec2fun  9973  acnlem  10127  dfac2a  10208  fin23lem14  10411  fin23lem16  10413  fin23lem17  10416  fin23lem38  10427  fin23lem39  10428  itunisuc  10497  axdc3lem2  10529  axcclem  10535  ac5b  10556  ttukey  10596  wunex2  10823  wuncval2  10832  intgru  10899  pnfex  11362  prdsvallem  17625  prdsval  17626  prdsds  17635  wunfunc  18076  wunnat  18134  arwval  18218  catcfuccl  18293  catcxpccl  18381  zrhval  21813  mreclatdemoBAD  23414  ptbasin2  23897  ptbasfi  23900  dfac14  23937  ptcmplem2  24372  ptcmplem3  24373  ptcmp  24377  cnextfvval  24384  cnextcn  24386  minveclem4a  25751  oldf  28223  precsexlem10  28602  xrge0tsmsbi  33635  dimval  34233  dimvalfi  34234  locfinreflem  34472  pstmfval  34528  pstmxmet  34529  esumex  34661  msrval  36303  dfrdg2  36557  fvbigcup  36664  ttctr  37281  ttcmin  37284  dfttc2g  37294  ctbssinf  38330  ptrest  38538  heiborlem1  38746  heiborlem3  38748  heibor  38756  dicval  42234  prjcrvfval  43668  aomclem1  44056  dfac21  44068  ntrrn  45122  ntrf  45123  dssmapntrcls  45128  permaxun  46001  fourierdlem70  47186  caragendifcl  47524  cnfsmf  47750  tposideq  49996