Theorem uniexg 7631

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 4859	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2822	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7630	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3514	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105  Vcvv 3441  ∪ cuni 4848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708  ax-sep 5236  ax-un 7626

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3443  df-in 3903  df-ss 3913  df-uni 4849

This theorem is referenced by:  uniex  7632  uniexd  7633  abnexg  7644  uniexb  7652  pwexr  7653  ssonuni  7668  ssonprc  7675  dmexg  7793  rnexg  7794  undefval  8137  onovuni  8218  tz7.44lem1  8281  tz7.44-3  8284  en1unielOLD  8869  disjen  8974  domss2  8976  fival  9239  fipwuni  9253  supexd  9280  cantnflem1  9515  dfac8clem  9858  onssnum  9866  dfac12lem1  9969  dfac12lem2  9970  fin1a2lem12  10237  hsmexlem1  10252  wrdexb  14297  restid  17211  prdsbas  17235  prdsplusg  17236  prdsmulr  17237  prdsvsca  17238  prdshom  17245  sscpwex  17594  pmtrfv  19127  istopon  22132  tgval  22176  eltg2  22179  tgss2  22208  neiptoptop  22353  restin  22388  restntr  22404  cnprest2  22512  pnrmopn  22565  cnrmnrm  22583  cmpsublem  22621  cmpsub  22622  cmpcld  22624  hausmapdom  22722  isref  22731  locfindis  22752  txbasex  22788  dfac14lem  22839  xkopt  22877  xkopjcn  22878  qtopval2  22918  elqtop  22919  fbssfi  23059  ptcmplem2  23275  cnextfval  23284  tuslem  23489  tuslemOLD  23490  pliguhgr  28956  acunirnmpt2  31105  acunirnmpt2f  31106  ist0cld  31889  hasheuni  32159  insiga  32211  sigagenval  32214  omsval  32366  omssubadd  32373  sibfof  32413  sitmcl  32424  kur14  33284  cvmscld  33341  madeval  34097  fobigcup  34263  hfuni  34547  isfne  34589  isfne4b  34591  fnemeet1  34616  tailfval  34622  bj-restuni2  35329  pibt2  35648  imaexALTV  36555  kelac2  41101  cnfex  42799  unidmex  42826  pwpwuni  42833  salgenval  44106  intsaluni  44112  salgenn0  44114  caragenunidm  44291  afv2ex  44965  iscnrm3rlem3  46495