Theorem uniex 7285

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

Syntax hints:   = wceq 1507   ∈ wcel 2050  Vcvv 3415  ∪ cuni 4713

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750  ax-sep 5061  ax-un 7281

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-rex 3094  df-v 3417  df-uni 4714

This theorem is referenced by:  vuniex  7286  unex  7288  iunpw  7311  elxp4  7444  elxp5  7445  1stval  7505  2ndval  7506  fo1st  7523  fo2nd  7524  cnvf1o  7616  brtpos2  7703  ixpsnf1o  8301  dffi3  8692  cnfcom2  8961  cnfcom3lem  8962  cnfcom3  8963  trcl  8966  rankc2  9096  rankxpl  9100  rankxpsuc  9107  acnlem  9270  dfac2a  9351  fin23lem14  9555  fin23lem16  9557  fin23lem17  9560  fin23lem38  9571  fin23lem39  9572  itunisuc  9641  axdc3lem2  9673  axcclem  9679  ac5b  9700  ttukey  9740  wunex2  9960  wuncval2  9969  intgru  10036  pnfex  10495  prdsval  16587  prdsds  16596  wunfunc  17030  wunnat  17087  arwval  17164  catcfuccl  17230  catcxpccl  17318  zrhval  20360  mreclatdemoBAD  21411  ptbasin2  21893  ptbasfi  21896  dfac14  21933  ptcmplem2  22368  ptcmplem3  22369  ptcmp  22373  cnextfvval  22380  cnextcn  22382  minveclem4a  23739  xrge0tsmsbi  30531  dimval  30630  dimvalfi  30631  locfinreflem  30748  pstmfval  30780  pstmxmet  30781  esumex  30932  msrval  32305  dfrdg2  32561  trpredex  32597  fvbigcup  32884  ctbssinf  34128  ptrest  34332  heiborlem1  34531  heiborlem3  34533  heibor  34541  dicval  37757  aomclem1  39050  dfac21  39062  ntrrn  39835  ntrf  39836  dssmapntrcls  39841  fourierdlem70  41893  caragendifcl  42228  cnfsmf  42449  setrec1lem3  44160  setrec2fun  44163