Theorem uniex 6995

Description: The Axiom of Union in class notation. This says that if 𝐴 is a set i.e. 𝐴 ∈ V (see isset 3238), 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

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		uniex.1	. 2 ⊢ 𝐴 ∈ V
2		unieq 4476	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
3	2	eleq1d 2715	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
4		uniex2 6994	. . 3 ⊢ ∃𝑦 𝑦 = ∪ 𝑥
5	4	issetri 3241	. 2 ⊢ ∪ 𝑥 ∈ V
6	1, 3, 5	vtocl 3290	1 ⊢ ∪ 𝐴 ∈ V

Syntax hints:   = wceq 1523   ∈ wcel 2030  Vcvv 3231  ∪ cuni 4468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-un 6991

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-v 3233  df-uni 4469

This theorem is referenced by:  vuniex  6996  unex  6998  iunpw  7020  elxp4  7152  elxp5  7153  1stval  7212  2ndval  7213  fo1st  7230  fo2nd  7231  cnvf1o  7321  brtpos2  7403  ixpsnf1o  7990  dffi3  8378  cnfcom2  8637  cnfcom3lem  8638  cnfcom3  8639  trcl  8642  rankc2  8772  rankxpl  8776  rankxpsuc  8783  acnlem  8909  dfac2a  8990  fin23lem14  9193  fin23lem16  9195  fin23lem17  9198  fin23lem38  9209  fin23lem39  9210  itunisuc  9279  axdc3lem2  9311  axcclem  9317  ac5b  9338  ttukey  9378  wunex2  9598  wuncval2  9607  intgru  9674  pnfxr  10130  prdsval  16162  prdsds  16171  wunfunc  16606  wunnat  16663  arwval  16740  catcfuccl  16806  catcxpccl  16894  zrhval  19904  mreclatdemoBAD  20948  ptbasin2  21429  ptbasfi  21432  dfac14  21469  ptcmplem2  21904  ptcmplem3  21905  ptcmp  21909  cnextfvval  21916  cnextcn  21918  minveclem4a  23247  xrge0tsmsbi  29914  locfinreflem  30035  pstmfval  30067  pstmxmet  30068  esumex  30219  msrval  31561  dfrdg2  31825  trpredex  31861  fvbigcup  32134  ptrest  33538  heiborlem1  33740  heiborlem3  33742  heibor  33750  dicval  36782  aomclem1  37941  dfac21  37953  ntrrn  38737  ntrf  38738  dssmapntrcls  38743  fourierdlem70  40711  caragendifcl  41049  cnfsmf  41270  setrec1lem3  42761  setrec2fun  42764