Theorem uniexg 7506

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 4816	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2815	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7505	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3471	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2112  Vcvv 3398  ∪ cuni 4805

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 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177  ax-un 7501

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870  df-uni 4806

This theorem is referenced by:  uniex  7507  uniexd  7508  abnexg  7519  uniexb  7527  pwexr  7528  ssonuni  7542  ssonprc  7549  dmexg  7659  rnexg  7660  undefval  7996  onovuni  8057  tz7.44lem1  8119  tz7.44-3  8122  en1unielOLD  8684  disjen  8781  domss2  8783  fival  9006  fipwuni  9020  supexd  9047  cantnflem1  9282  dfac8clem  9611  onssnum  9619  dfac12lem1  9722  dfac12lem2  9723  fin1a2lem12  9990  hsmexlem1  10005  wrdexb  14045  restid  16892  prdsbas  16916  prdsplusg  16917  prdsmulr  16918  prdsvsca  16919  prdshom  16926  sscpwex  17274  pmtrfv  18798  istopon  21763  tgval  21806  eltg2  21809  tgss2  21838  neiptoptop  21982  restin  22017  restntr  22033  cnprest2  22141  pnrmopn  22194  cnrmnrm  22212  cmpsublem  22250  cmpsub  22251  cmpcld  22253  hausmapdom  22351  isref  22360  locfindis  22381  txbasex  22417  dfac14lem  22468  xkopt  22506  xkopjcn  22507  qtopval2  22547  elqtop  22548  fbssfi  22688  ptcmplem2  22904  cnextfval  22913  tuslem  23118  pliguhgr  28521  acunirnmpt2  30671  acunirnmpt2f  30672  ist0cld  31451  hasheuni  31719  insiga  31771  sigagenval  31774  omsval  31926  omssubadd  31933  sibfof  31973  sitmcl  31984  kur14  32845  cvmscld  32902  madeval  33722  fobigcup  33888  hfuni  34172  isfne  34214  isfne4b  34216  fnemeet1  34241  tailfval  34247  bj-restuni2  34953  pibt2  35274  imaexALTV  36151  kelac2  40534  cnfex  42185  unidmex  42212  pwpwuni  42219  salgenval  43480  intsaluni  43486  salgenn0  43488  caragenunidm  43664  afv2ex  44321  iscnrm3rlem3  45852