Theorem uniexg 7745

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

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

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 2734  ax-sep 5255  ax-un 7739

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-uni 4871

This theorem is used by:  uniex  7746  uniexd  7747  abnexg  7758  uniexb  7766  pwexr  7767  ssonuni  7782  ssonprc  7789  dmexg  7901  rnexg  7902  undefval  8278  onovuni  8334  tz7.44lem1  8397  tz7.44-3  8400  disjen  9135  domss2  9137  fival  9385  fipwuni  9399  supexd  9426  cantnflem1  9671  dfac8clem  10038  onssnum  10046  dfac12lem1  10149  dfac12lem2  10150  fin1a2lem12  10416  hsmexlem1  10431  wrdexb  14592  restid  17522  prdsbas  17546  prdsplusg  17547  prdsmulr  17548  prdsvsca  17549  prdshom  17556  sscpwex  17908  pmtrfv  19580  istopon  23138  tgval  23181  eltg2  23184  tgss2  23213  neiptoptop  23357  restin  23392  restntr  23408  cnprest2  23516  pnrmopn  23569  cnrmnrm  23587  cmpsublem  23625  cmpsub  23626  cmpcld  23628  hausmapdom  23727  isref  23736  locfindis  23757  txbasex  23793  dfac14lem  23844  xkopt  23882  xkopjcn  23883  qtopval2  23923  elqtop  23924  fbssfi  24064  ptcmplem2  24280  cnextfval  24289  tuslem  24493  madeval  28095  pliguhgr  30953  acunirnmpt2  33120  acunirnmpt2f  33121  ist0cld  34330  hasheuni  34582  insiga  34635  sigagenval  34638  omsval  34791  omssubadd  34798  sibfof  34838  sitmcl  34849  kur14  35782  cvmscld  35839  fobigcup  36464  hfuni  36751  isfne  36945  isfne4b  36947  fnemeet1  36972  tailfval  36978  bj-restuni2  37835  pibt2  38158  kelac2  43893  cnfex  45849  unidmex  45871  pwpwuni  45878  salgenval  47136  intsaluni  47144  salgenn0  47146  caragenunidm  47323  afv2ex  48089  iscnrm3rlem3  49855