Theorem uniexg 7687

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 4852	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2826	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7686	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3502	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1548   ∈ wcel 2121  Vcvv 3433  ∪ cuni 4841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-un 7682

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3902  df-uni 4842

This theorem is referenced by:  uniex  7688  uniexd  7689  abnexg  7703  uniexb  7711  pwexr  7712  ssonuni  7727  ssonprc  7734  dmexg  7845  rnexg  7846  undefval  8220  onovuni  8276  tz7.44lem1  8338  tz7.44-3  8341  disjen  9066  domss2  9068  fival  9319  fipwuni  9333  supexd  9360  cantnflem1  9605  dfac8clem  9949  onssnum  9957  dfac12lem1  10061  dfac12lem2  10062  fin1a2lem12  10328  hsmexlem1  10343  wrdexb  14482  restid  17391  prdsbas  17415  prdsplusg  17416  prdsmulr  17417  prdsvsca  17418  prdshom  17425  sscpwex  17777  pmtrfv  19422  istopon  22899  tgval  22942  eltg2  22945  tgss2  22974  neiptoptop  23118  restin  23153  restntr  23169  cnprest2  23277  pnrmopn  23330  cnrmnrm  23348  cmpsublem  23386  cmpsub  23387  cmpcld  23389  hausmapdom  23487  isref  23496  locfindis  23517  txbasex  23553  dfac14lem  23604  xkopt  23642  xkopjcn  23643  qtopval2  23683  elqtop  23684  fbssfi  23824  ptcmplem2  24040  cnextfval  24049  tuslem  24253  madeval  27846  pliguhgr  30579  acunirnmpt2  32756  acunirnmpt2f  32757  ist0cld  34029  hasheuni  34281  insiga  34333  sigagenval  34336  omsval  34489  omssubadd  34496  sibfof  34536  sitmcl  34547  kur14  35459  cvmscld  35516  fobigcup  36141  hfuni  36427  isfne  36582  isfne4b  36584  fnemeet1  36609  tailfval  36615  bj-restuni2  37471  pibt2  37794  kelac2  43525  cnfex  45491  unidmex  45513  pwpwuni  45520  salgenval  46778  intsaluni  46786  salgenn0  46788  caragenunidm  46965  afv2ex  47691  iscnrm3rlem3  49446