Theorem uniexg 7750

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 4923	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2810	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7749	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3533	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  Vcvv 3461  ∪ cuni 4912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5303  ax-un 7745

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-ss 3963  df-uni 4913

This theorem is referenced by:  uniex  7751  uniexd  7752  abnexg  7763  uniexb  7771  pwexr  7772  ssonuni  7787  ssonprc  7795  dmexg  7913  rnexg  7914  undefval  8290  onovuni  8371  tz7.44lem1  8434  tz7.44-3  8437  en1unielOLD  9064  disjen  9171  domss2  9173  fival  9451  fipwuni  9465  supexd  9492  cantnflem1  9728  dfac8clem  10071  onssnum  10079  dfac12lem1  10182  dfac12lem2  10183  fin1a2lem12  10450  hsmexlem1  10465  wrdexb  14528  restid  17443  prdsbas  17467  prdsplusg  17468  prdsmulr  17469  prdsvsca  17470  prdshom  17477  sscpwex  17826  pmtrfv  19445  istopon  22897  tgval  22941  eltg2  22944  tgss2  22973  neiptoptop  23118  restin  23153  restntr  23169  cnprest2  23277  pnrmopn  23330  cnrmnrm  23348  cmpsublem  23386  cmpsub  23387  cmpcld  23389  hausmapdom  23487  isref  23496  locfindis  23517  txbasex  23553  dfac14lem  23604  xkopt  23642  xkopjcn  23643  qtopval2  23683  elqtop  23684  fbssfi  23824  ptcmplem2  24040  cnextfval  24049  tuslem  24254  tuslemOLD  24255  madeval  27868  pliguhgr  30411  acunirnmpt2  32568  acunirnmpt2f  32569  ist0cld  33604  hasheuni  33874  insiga  33926  sigagenval  33929  omsval  34083  omssubadd  34090  sibfof  34130  sitmcl  34141  kur14  34996  cvmscld  35053  fobigcup  35672  hfuni  35956  isfne  35999  isfne4b  36001  fnemeet1  36026  tailfval  36032  bj-restuni2  36753  pibt2  37072  imaexALTV  37976  kelac2  42663  cnfex  44564  unidmex  44588  pwpwuni  44595  salgenval  45879  intsaluni  45887  salgenn0  45889  caragenunidm  46066  afv2ex  46764  iscnrm3rlem3  48213