Theorem uniexg 7739

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 4885	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2854	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7738	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3529	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  Vcvv 3461  ∪ cuni 4874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5259  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3463  df-ss 3928  df-uni 4875

This theorem is referenced by:  uniex  7740  uniexd  7741  abnexg  7755  uniexb  7763  pwexr  7764  ssonuni  7779  ssonprc  7786  dmexg  7898  rnexg  7899  undefval  8273  onovuni  8329  tz7.44lem1  8392  tz7.44-3  8395  disjen  9122  domss2  9124  fival  9372  fipwuni  9386  supexd  9413  cantnflem1  9658  dfac8clem  10016  onssnum  10024  dfac12lem1  10127  dfac12lem2  10128  fin1a2lem12  10395  hsmexlem1  10410  wrdexb  14562  restid  17486  prdsbas  17510  prdsplusg  17511  prdsmulr  17512  prdsvsca  17513  prdshom  17520  sscpwex  17872  pmtrfv  19522  istopon  23038  tgval  23081  eltg2  23084  tgss2  23113  neiptoptop  23257  restin  23292  restntr  23308  cnprest2  23416  pnrmopn  23469  cnrmnrm  23487  cmpsublem  23525  cmpsub  23526  cmpcld  23528  hausmapdom  23626  isref  23635  locfindis  23656  txbasex  23692  dfac14lem  23743  xkopt  23781  xkopjcn  23782  qtopval2  23822  elqtop  23823  fbssfi  23963  ptcmplem2  24179  cnextfval  24188  tuslem  24392  madeval  27991  pliguhgr  30779  acunirnmpt2  32946  acunirnmpt2f  32947  ist0cld  34168  hasheuni  34420  insiga  34472  sigagenval  34475  omsval  34628  omssubadd  34635  sibfof  34675  sitmcl  34686  kur14  35641  cvmscld  35698  fobigcup  36323  hfuni  36609  isfne  36773  isfne4b  36775  fnemeet1  36800  tailfval  36806  bj-restuni2  37663  pibt2  37986  kelac2  43719  cnfex  45675  unidmex  45697  pwpwuni  45704  salgenval  46962  intsaluni  46970  salgenn0  46972  caragenunidm  47149  afv2ex  47875  iscnrm3rlem3  49640