Theorem uniexg 7689

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3430  ∪ cuni 4851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-un 7684

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-uni 4852

This theorem is referenced by:  uniex  7690  uniexd  7691  abnexg  7705  uniexb  7713  pwexr  7714  ssonuni  7729  ssonprc  7736  dmexg  7847  rnexg  7848  undefval  8221  onovuni  8277  tz7.44lem1  8339  tz7.44-3  8342  disjen  9067  domss2  9069  fival  9320  fipwuni  9334  supexd  9361  cantnflem1  9605  dfac8clem  9949  onssnum  9957  dfac12lem1  10061  dfac12lem2  10062  fin1a2lem12  10328  hsmexlem1  10343  wrdexb  14482  restid  17391  prdsbas  17415  prdsplusg  17416  prdsmulr  17417  prdsvsca  17418  prdshom  17425  sscpwex  17777  pmtrfv  19422  istopon  22891  tgval  22934  eltg2  22937  tgss2  22966  neiptoptop  23110  restin  23145  restntr  23161  cnprest2  23269  pnrmopn  23322  cnrmnrm  23340  cmpsublem  23378  cmpsub  23379  cmpcld  23381  hausmapdom  23479  isref  23488  locfindis  23509  txbasex  23545  dfac14lem  23596  xkopt  23634  xkopjcn  23635  qtopval2  23675  elqtop  23676  fbssfi  23816  ptcmplem2  24032  cnextfval  24041  tuslem  24245  madeval  27842  pliguhgr  30576  acunirnmpt2  32752  acunirnmpt2f  32753  ist0cld  33997  hasheuni  34249  insiga  34301  sigagenval  34304  omsval  34457  omssubadd  34464  sibfof  34504  sitmcl  34515  kur14  35418  cvmscld  35475  fobigcup  36100  hfuni  36386  isfne  36541  isfne4b  36543  fnemeet1  36568  tailfval  36574  bj-restuni2  37430  pibt2  37753  kelac2  43517  cnfex  45483  unidmex  45505  pwpwuni  45512  salgenval  46773  intsaluni  46781  salgenn0  46783  caragenunidm  46960  afv2ex  47680  iscnrm3rlem3  49435