Theorem uniex 7779

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  ∪ 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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-un 7772

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4871

This theorem is used by:  iunpw  7806  elxp4  7955  elxp5  7956  1stval  8024  2ndval  8025  fo1st  8042  fo2nd  8043  cnvf1o  8146  brtpos2  8274  naddcllem  8710  ixpsnf1o  8991  dffi3  9447  cnfcom2  9727  cnfcom3lem  9728  cnfcom3  9729  ttrclse  9752  trcl  9753  rankc2  9912  rankxpl  9916  rankxpsuc  9923  setrec1lem3  9993  setrec2fun  9997  acnlem  10151  dfac2a  10232  fin23lem14  10435  fin23lem16  10437  fin23lem17  10440  fin23lem38  10451  fin23lem39  10452  itunisuc  10521  axdc3lem2  10553  axcclem  10559  ac5b  10580  ttukey  10620  wunex2  10847  wuncval2  10856  intgru  10923  pnfex  11386  prdsvallem  17651  prdsval  17652  prdsds  17661  wunfunc  18102  wunnat  18160  arwval  18244  catcfuccl  18319  catcxpccl  18407  zrhval  21840  mreclatdemoBAD  23441  ptbasin2  23924  ptbasfi  23927  dfac14  23964  ptcmplem2  24399  ptcmplem3  24400  ptcmp  24404  cnextfvval  24411  cnextcn  24413  minveclem4a  25778  oldf  28250  precsexlem10  28629  xrge0tsmsbi  33702  dimval  34300  dimvalfi  34301  locfinreflem  34539  pstmfval  34595  pstmxmet  34596  esumex  34728  msrval  36469  dfrdg2  36734  fvbigcup  36841  ttctr  37458  ttcmin  37461  dfttc2g  37471  ctbssinf  38520  ptrest  38728  heiborlem1  38936  heiborlem3  38938  heibor  38946  dicval  42424  prjcrvfval  43858  aomclem1  44247  dfac21  44259  ntrrn  45312  ntrf  45313  dssmapntrcls  45318  permaxun  46194  fourierdlem70  47389  caragendifcl  47727  cnfsmf  47953  tposideq  50204