Theorem uniex 7742

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 7741	. 2 ⊢ (𝐴 ∈ V → ∪ 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ ∪ 𝐴 ∈ V

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  ∪ cuni 4867

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 2732  ax-sep 5249  ax-un 7735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-uni 4868

This theorem is used by:  iunpw  7769  elxp4  7918  elxp5  7919  1stval  7987  2ndval  7988  fo1st  8005  fo2nd  8006  cnvf1o  8106  brtpos2  8228  naddcllem  8664  ixpsnf1o  8945  dffi3  9401  cnfcom2  9681  cnfcom3lem  9682  cnfcom3  9683  ttrclse  9706  trcl  9707  rankc2  9857  rankxpl  9861  rankxpsuc  9868  setrec1lem3  9926  setrec2fun  9930  acnlem  10084  dfac2a  10165  fin23lem14  10368  fin23lem16  10370  fin23lem17  10373  fin23lem38  10384  fin23lem39  10385  itunisuc  10454  axdc3lem2  10486  axcclem  10492  ac5b  10513  ttukey  10553  wunex2  10780  wuncval2  10789  intgru  10856  pnfex  11319  prdsvallem  17572  prdsval  17573  prdsds  17582  wunfunc  18023  wunnat  18081  arwval  18165  catcfuccl  18240  catcxpccl  18328  zrhval  21760  mreclatdemoBAD  23361  ptbasin2  23844  ptbasfi  23847  dfac14  23884  ptcmplem2  24319  ptcmplem3  24320  ptcmp  24324  cnextfvval  24331  cnextcn  24333  minveclem4a  25698  oldf  28142  precsexlem10  28521  xrge0tsmsbi  33554  dimval  34152  dimvalfi  34153  locfinreflem  34391  pstmfval  34447  pstmxmet  34448  esumex  34580  msrval  36218  dfrdg2  36473  fvbigcup  36580  ttctr  37197  ttcmin  37200  dfttc2g  37210  ctbssinf  38243  ptrest  38451  heiborlem1  38659  heiborlem3  38661  heibor  38669  dicval  42147  prjcrvfval  43575  aomclem1  43993  dfac21  44005  ntrrn  45060  ntrf  45061  dssmapntrcls  45066  permaxun  45932  fourierdlem70  47102  caragendifcl  47440  cnfsmf  47666  tposideq  49912