Theorem uniexg 7716

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3447  ∪ cuni 4871

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 5251  ax-un 7711

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 3449  df-ss 3931  df-uni 4872

This theorem is referenced by:  uniex  7717  uniexd  7718  abnexg  7732  uniexb  7740  pwexr  7741  ssonuni  7756  ssonprc  7763  dmexg  7877  rnexg  7878  undefval  8255  onovuni  8311  tz7.44lem1  8373  tz7.44-3  8376  disjen  9098  domss2  9100  fival  9363  fipwuni  9377  supexd  9404  cantnflem1  9642  dfac8clem  9985  onssnum  9993  dfac12lem1  10097  dfac12lem2  10098  fin1a2lem12  10364  hsmexlem1  10379  wrdexb  14490  restid  17396  prdsbas  17420  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  prdshom  17430  sscpwex  17777  pmtrfv  19382  istopon  22799  tgval  22842  eltg2  22845  tgss2  22874  neiptoptop  23018  restin  23053  restntr  23069  cnprest2  23177  pnrmopn  23230  cnrmnrm  23248  cmpsublem  23286  cmpsub  23287  cmpcld  23289  hausmapdom  23387  isref  23396  locfindis  23417  txbasex  23453  dfac14lem  23504  xkopt  23542  xkopjcn  23543  qtopval2  23583  elqtop  23584  fbssfi  23724  ptcmplem2  23940  cnextfval  23949  tuslem  24154  madeval  27760  pliguhgr  30415  acunirnmpt2  32584  acunirnmpt2f  32585  ist0cld  33823  hasheuni  34075  insiga  34127  sigagenval  34130  omsval  34284  omssubadd  34291  sibfof  34331  sitmcl  34342  kur14  35203  cvmscld  35260  fobigcup  35888  hfuni  36172  isfne  36327  isfne4b  36329  fnemeet1  36354  tailfval  36360  bj-restuni2  37086  pibt2  37405  kelac2  43054  cnfex  45022  unidmex  45044  pwpwuni  45051  salgenval  46319  intsaluni  46327  salgenn0  46329  caragenunidm  46506  afv2ex  47215  iscnrm3rlem3  48930