Theorem uniexg 7676

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 4869	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2813	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7675	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3509	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3436  ∪ cuni 4858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-uni 4859

This theorem is referenced by:  uniex  7677  uniexd  7678  abnexg  7692  uniexb  7700  pwexr  7701  ssonuni  7716  ssonprc  7723  dmexg  7834  rnexg  7835  undefval  8209  onovuni  8265  tz7.44lem1  8327  tz7.44-3  8330  disjen  9051  domss2  9053  fival  9302  fipwuni  9316  supexd  9343  cantnflem1  9585  dfac8clem  9926  onssnum  9934  dfac12lem1  10038  dfac12lem2  10039  fin1a2lem12  10305  hsmexlem1  10320  wrdexb  14432  restid  17337  prdsbas  17361  prdsplusg  17362  prdsmulr  17363  prdsvsca  17364  prdshom  17371  sscpwex  17722  pmtrfv  19331  istopon  22797  tgval  22840  eltg2  22843  tgss2  22872  neiptoptop  23016  restin  23051  restntr  23067  cnprest2  23175  pnrmopn  23228  cnrmnrm  23246  cmpsublem  23284  cmpsub  23285  cmpcld  23287  hausmapdom  23385  isref  23394  locfindis  23415  txbasex  23451  dfac14lem  23502  xkopt  23540  xkopjcn  23541  qtopval2  23581  elqtop  23582  fbssfi  23722  ptcmplem2  23938  cnextfval  23947  tuslem  24152  madeval  27764  pliguhgr  30434  acunirnmpt2  32611  acunirnmpt2f  32612  ist0cld  33816  hasheuni  34068  insiga  34120  sigagenval  34123  omsval  34277  omssubadd  34284  sibfof  34324  sitmcl  34335  kur14  35209  cvmscld  35266  fobigcup  35894  hfuni  36178  isfne  36333  isfne4b  36335  fnemeet1  36360  tailfval  36366  bj-restuni2  37092  pibt2  37411  kelac2  43058  cnfex  45026  unidmex  45048  pwpwuni  45055  salgenval  46322  intsaluni  46330  salgenn0  46332  caragenunidm  46509  afv2ex  47218  iscnrm3rlem3  48946