Theorem uniex 7588

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

Syntax hints:   ∈ wcel 2110  Vcvv 3431  ∪ cuni 4845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-sep 5227  ax-un 7582

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-in 3899  df-ss 3909  df-uni 4846

This theorem is referenced by:  unex  7590  iunpw  7615  elxp4  7763  elxp5  7764  1stval  7826  2ndval  7827  fo1st  7844  fo2nd  7845  cnvf1o  7942  brtpos2  8039  ixpsnf1o  8709  dffi3  9168  cnfcom2  9438  cnfcom3lem  9439  cnfcom3  9440  ttrclse  9463  trpredex  9485  trcl  9486  rankc2  9630  rankxpl  9634  rankxpsuc  9641  acnlem  9805  dfac2a  9886  fin23lem14  10090  fin23lem16  10092  fin23lem17  10095  fin23lem38  10106  fin23lem39  10107  itunisuc  10176  axdc3lem2  10208  axcclem  10214  ac5b  10235  ttukey  10275  wunex2  10495  wuncval2  10504  intgru  10571  pnfex  11029  prdsvallem  17163  prdsval  17164  prdsds  17173  wunfunc  17612  wunfuncOLD  17613  wunnat  17670  wunnatOLD  17671  arwval  17756  catcfuccl  17832  catcfucclOLD  17833  catcxpccl  17922  catcxpcclOLD  17923  zrhval  20707  mreclatdemoBAD  22245  ptbasin2  22727  ptbasfi  22730  dfac14  22767  ptcmplem2  23202  ptcmplem3  23203  ptcmp  23207  cnextfvval  23214  cnextcn  23216  minveclem4a  24592  xrge0tsmsbi  31314  dimval  31682  dimvalfi  31683  locfinreflem  31786  pstmfval  31842  pstmxmet  31843  esumex  31993  msrval  33496  dfrdg2  33767  naddcllem  33827  oldf  34037  fvbigcup  34200  ctbssinf  35573  ptrest  35772  heiborlem1  35965  heiborlem3  35967  heibor  35975  dicval  39186  prjcrvfval  40465  aomclem1  40876  dfac21  40888  ntrrn  41702  ntrf  41703  dssmapntrcls  41708  fourierdlem70  43688  caragendifcl  44023  cnfsmf  44244  setrec1lem3  46364  setrec2fun  46367