Theorem uniex 7743

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

Syntax hints:   ∈ wcel 2107  Vcvv 3463  ∪ cuni 4887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5276  ax-un 7737

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3465  df-ss 3948  df-uni 4888

This theorem is referenced by:  unexOLD  7747  iunpw  7773  elxp4  7926  elxp5  7927  1stval  7998  2ndval  7999  fo1st  8016  fo2nd  8017  cnvf1o  8118  brtpos2  8239  naddcllem  8696  ixpsnf1o  8960  dffi3  9453  cnfcom2  9724  cnfcom3lem  9725  cnfcom3  9726  ttrclse  9749  trcl  9750  rankc2  9893  rankxpl  9897  rankxpsuc  9904  acnlem  10070  dfac2a  10152  fin23lem14  10355  fin23lem16  10357  fin23lem17  10360  fin23lem38  10371  fin23lem39  10372  itunisuc  10441  axdc3lem2  10473  axcclem  10479  ac5b  10500  ttukey  10540  wunex2  10760  wuncval2  10769  intgru  10836  pnfex  11296  prdsvallem  17471  prdsval  17472  prdsds  17481  wunfunc  17918  wunnat  17976  arwval  18060  catcfuccl  18135  catcxpccl  18223  zrhval  21481  mreclatdemoBAD  23051  ptbasin2  23533  ptbasfi  23536  dfac14  23573  ptcmplem2  24008  ptcmplem3  24009  ptcmp  24013  cnextfvval  24020  cnextcn  24022  minveclem4a  25401  oldf  27833  madefi  27887  precsexlem10  28177  xrge0tsmsbi  33010  dimval  33591  dimvalfi  33592  locfinreflem  33814  pstmfval  33870  pstmxmet  33871  esumex  34005  msrval  35518  dfrdg2  35771  fvbigcup  35878  ctbssinf  37382  ptrest  37601  heiborlem1  37793  heiborlem3  37795  heibor  37803  dicval  41153  prjcrvfval  42620  aomclem1  43044  dfac21  43056  ntrrn  44112  ntrf  44113  dssmapntrcls  44118  fourierdlem70  46163  caragendifcl  46501  cnfsmf  46727  tposideq  48771  setrec1lem3  49303  setrec2fun  49306