Theorem uniexg 7685

Description: The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent 𝐴 ∈ 𝑉 instead of 𝐴 ∈ V to make the theorem more general and thus shorten some proofs; obviously the universal class constant V is one possible substitution for class variable 𝑉. (Contributed by NM, 25-Nov-1994.)

Assertion

Ref	Expression
uniexg	⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Proof of Theorem uniexg

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		unieq 4873	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2820	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7684	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3510	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3439  ∪ cuni 4862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5240  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3441  df-ss 3917  df-uni 4863

This theorem is referenced by:  uniex  7686  uniexd  7687  abnexg  7701  uniexb  7709  pwexr  7710  ssonuni  7725  ssonprc  7732  dmexg  7843  rnexg  7844  undefval  8218  onovuni  8274  tz7.44lem1  8336  tz7.44-3  8339  disjen  9064  domss2  9066  fival  9317  fipwuni  9331  supexd  9358  cantnflem1  9600  dfac8clem  9944  onssnum  9952  dfac12lem1  10056  dfac12lem2  10057  fin1a2lem12  10323  hsmexlem1  10338  wrdexb  14450  restid  17355  prdsbas  17379  prdsplusg  17380  prdsmulr  17381  prdsvsca  17382  prdshom  17389  sscpwex  17741  pmtrfv  19383  istopon  22858  tgval  22901  eltg2  22904  tgss2  22933  neiptoptop  23077  restin  23112  restntr  23128  cnprest2  23236  pnrmopn  23289  cnrmnrm  23307  cmpsublem  23345  cmpsub  23346  cmpcld  23348  hausmapdom  23446  isref  23455  locfindis  23476  txbasex  23512  dfac14lem  23563  xkopt  23601  xkopjcn  23602  qtopval2  23642  elqtop  23643  fbssfi  23783  ptcmplem2  23999  cnextfval  24008  tuslem  24212  madeval  27828  pliguhgr  30542  acunirnmpt2  32718  acunirnmpt2f  32719  ist0cld  33969  hasheuni  34221  insiga  34273  sigagenval  34276  omsval  34429  omssubadd  34436  sibfof  34476  sitmcl  34487  kur14  35389  cvmscld  35446  fobigcup  36071  hfuni  36357  isfne  36512  isfne4b  36514  fnemeet1  36539  tailfval  36545  bj-restuni2  37272  pibt2  37591  kelac2  43344  cnfex  45310  unidmex  45332  pwpwuni  45339  salgenval  46602  intsaluni  46610  salgenn0  46612  caragenunidm  46789  afv2ex  47497  iscnrm3rlem3  49224