Theorem uniexg 7740

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  Vcvv 3450  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5248  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3915  df-uni 4867

This theorem is used by:  uniex  7741  uniexd  7742  abnexg  7753  uniexb  7761  pwexr  7762  ssonuni  7777  ssonprc  7784  dmexg  7896  rnexg  7897  undefval  8272  onovuni  8328  tz7.44lem1  8391  tz7.44-3  8394  disjen  9131  domss2  9133  fival  9382  fipwuni  9396  supexd  9423  cantnflem1  9668  hfuniOLD  9896  dfac8clem  10082  onssnum  10090  dfac12lem1  10193  dfac12lem2  10194  fin1a2lem12  10460  hsmexlem1  10475  wrdexb  14637  restid  17565  prdsbas  17589  prdsplusg  17590  prdsmulr  17591  prdsvsca  17592  prdshom  17599  sscpwex  17951  pmtrfv  19627  istopon  23191  tgval  23234  eltg2  23237  tgss2  23266  neiptoptop  23410  restin  23445  restntr  23461  cnprest2  23569  pnrmopn  23622  cnrmnrm  23640  cmpsublem  23678  cmpsub  23679  cmpcld  23681  hausmapdom  23780  isref  23789  locfindis  23810  txbasex  23846  dfac14lem  23897  xkopt  23935  xkopjcn  23936  qtopval2  23976  elqtop  23977  fbssfi  24117  ptcmplem2  24333  cnextfval  24342  tuslem  24546  madeval  28151  pliguhgr  31021  acunirnmpt2  33187  acunirnmpt2f  33188  ist0cld  34398  hasheuni  34650  insiga  34703  sigagenval  34706  omsval  34859  omssubadd  34866  sibfof  34906  sitmcl  34917  kur14  35902  cvmscld  35959  fobigcup  36584  isfne  37049  isfne4b  37051  fnemeet1  37076  tailfval  37082  bj-restuni2  37939  pibt2  38260  kelac2  44010  cnfex  45966  unidmex  45988  pwpwuni  45995  salgenval  47253  intsaluni  47261  salgenn0  47263  caragenunidm  47440  afv2ex  48206  iscnrm3rlem3  49972