Theorem uniexg 7696

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3444  ∪ cuni 4867

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 5246  ax-un 7691

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 3446  df-ss 3928  df-uni 4868

This theorem is referenced by:  uniex  7697  uniexd  7698  abnexg  7712  uniexb  7720  pwexr  7721  ssonuni  7736  ssonprc  7743  dmexg  7857  rnexg  7858  undefval  8232  onovuni  8288  tz7.44lem1  8350  tz7.44-3  8353  disjen  9075  domss2  9077  fival  9339  fipwuni  9353  supexd  9380  cantnflem1  9618  dfac8clem  9961  onssnum  9969  dfac12lem1  10073  dfac12lem2  10074  fin1a2lem12  10340  hsmexlem1  10355  wrdexb  14466  restid  17372  prdsbas  17396  prdsplusg  17397  prdsmulr  17398  prdsvsca  17399  prdshom  17406  sscpwex  17757  pmtrfv  19366  istopon  22832  tgval  22875  eltg2  22878  tgss2  22907  neiptoptop  23051  restin  23086  restntr  23102  cnprest2  23210  pnrmopn  23263  cnrmnrm  23281  cmpsublem  23319  cmpsub  23320  cmpcld  23322  hausmapdom  23420  isref  23429  locfindis  23450  txbasex  23486  dfac14lem  23537  xkopt  23575  xkopjcn  23576  qtopval2  23616  elqtop  23617  fbssfi  23757  ptcmplem2  23973  cnextfval  23982  tuslem  24187  madeval  27797  pliguhgr  30465  acunirnmpt2  32634  acunirnmpt2f  32635  ist0cld  33816  hasheuni  34068  insiga  34120  sigagenval  34123  omsval  34277  omssubadd  34284  sibfof  34324  sitmcl  34335  kur14  35196  cvmscld  35253  fobigcup  35881  hfuni  36165  isfne  36320  isfne4b  36322  fnemeet1  36347  tailfval  36353  bj-restuni2  37079  pibt2  37398  kelac2  43047  cnfex  45015  unidmex  45037  pwpwuni  45044  salgenval  46312  intsaluni  46320  salgenn0  46322  caragenunidm  46499  afv2ex  47208  iscnrm3rlem3  48923