Theorem uniex 6953

Description: The Axiom of Union in class notation. This says that if 𝐴 is a set i.e. 𝐴 ∈ V (see isset 3207), 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 4444	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
3	2	eleq1d 2686	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
4		uniex2 6952	. . 3 ⊢ ∃𝑦 𝑦 = ∪ 𝑥
5	4	issetri 3210	. 2 ⊢ ∪ 𝑥 ∈ V
6	1, 3, 5	vtocl 3259	1 ⊢ ∪ 𝐴 ∈ V

Syntax hints:   = wceq 1483   ∈ wcel 1990  Vcvv 3200  ∪ cuni 4436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-v 3202  df-uni 4437

This theorem is referenced by:  vuniex  6954  unex  6956  iunpw  6978  elxp4  7110  elxp5  7111  1stval  7170  2ndval  7171  fo1st  7188  fo2nd  7189  cnvf1o  7276  brtpos2  7358  ixpsnf1o  7948  dffi3  8337  cnfcom2  8599  cnfcom3lem  8600  cnfcom3  8601  trcl  8604  rankc2  8734  rankxpl  8738  rankxpsuc  8745  acnlem  8871  dfac2a  8952  fin23lem14  9155  fin23lem16  9157  fin23lem17  9160  fin23lem38  9171  fin23lem39  9172  itunisuc  9241  axdc3lem2  9273  axcclem  9279  ac5b  9300  ttukey  9340  wunex2  9560  wuncval2  9569  intgru  9636  pnfxr  10092  prdsval  16115  prdsds  16124  wunfunc  16559  wunnat  16616  arwval  16693  catcfuccl  16759  catcxpccl  16847  zrhval  19856  mreclatdemoBAD  20900  ptbasin2  21381  ptbasfi  21384  dfac14  21421  ptcmplem2  21857  ptcmplem3  21858  ptcmp  21862  cnextfvval  21869  cnextcn  21871  minveclem4a  23201  xrge0tsmsbi  29786  locfinreflem  29907  pstmfval  29939  pstmxmet  29940  esumex  30091  msrval  31435  dfrdg2  31701  trpredex  31737  fvbigcup  32009  ptrest  33408  heiborlem1  33610  heiborlem3  33612  heibor  33620  dicval  36465  aomclem1  37624  dfac21  37636  ntrrn  38420  ntrf  38421  dssmapntrcls  38426  fourierdlem70  40393  caragendifcl  40728  cnfsmf  40949  setrec1lem3  42436  setrec2fun  42439