Theorem uniex 7741

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

This proof depends on syntax axioms:   ∈ wcel 2142  Vcvv 3454  ∪ cuni 4871

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-uni 4872

This theorem is used by:  iunpw  7768  elxp4  7917  elxp5  7918  1stval  7986  2ndval  7987  fo1st  8004  fo2nd  8005  cnvf1o  8104  brtpos2  8226  naddcllem  8660  ixpsnf1o  8934  dffi3  9389  cnfcom2  9669  cnfcom3lem  9670  cnfcom3  9671  ttrclse  9694  trcl  9695  rankc2  9841  rankxpl  9845  rankxpsuc  9852  acnlem  10039  dfac2a  10120  fin23lem14  10323  fin23lem16  10325  fin23lem17  10328  fin23lem38  10339  fin23lem39  10340  itunisuc  10409  axdc3lem2  10441  axcclem  10447  ac5b  10468  ttukey  10508  wunex2  10729  wuncval2  10738  intgru  10805  pnfex  11268  prdsvallem  17513  prdsval  17514  prdsds  17523  wunfunc  17964  wunnat  18022  arwval  18106  catcfuccl  18181  catcxpccl  18269  zrhval  21668  mreclatdemoBAD  23264  ptbasin2  23746  ptbasfi  23749  dfac14  23786  ptcmplem2  24221  ptcmplem3  24222  ptcmp  24226  cnextfvval  24233  cnextcn  24235  minveclem4a  25600  oldf  28041  madefi  28117  precsexlem10  28420  xrge0tsmsbi  33403  dimval  34000  dimvalfi  34001  locfinreflem  34239  pstmfval  34295  pstmxmet  34296  esumex  34428  msrval  36038  dfrdg2  36293  fvbigcup  36400  ttctr  37032  ttcmin  37035  dfttc2g  37045  ctbssinf  38080  ptrest  38298  heiborlem1  38490  heiborlem3  38492  heibor  38500  dicval  41978  prjcrvfval  43391  aomclem1  43809  dfac21  43821  ntrrn  44876  ntrf  44877  dssmapntrcls  44882  permaxun  45748  fourierdlem70  46918  caragendifcl  47256  cnfsmf  47482  tposideq  49694  setrec1lem3  50495  setrec2fun  50498