Theorem uniexg 7697

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3442  ∪ cuni 4865

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 5245  ax-un 7692

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 3444  df-ss 3920  df-uni 4866

This theorem is referenced by:  uniex  7698  uniexd  7699  abnexg  7713  uniexb  7721  pwexr  7722  ssonuni  7737  ssonprc  7744  dmexg  7855  rnexg  7856  undefval  8230  onovuni  8286  tz7.44lem1  8348  tz7.44-3  8351  disjen  9076  domss2  9078  fival  9329  fipwuni  9343  supexd  9370  cantnflem1  9612  dfac8clem  9956  onssnum  9964  dfac12lem1  10068  dfac12lem2  10069  fin1a2lem12  10335  hsmexlem1  10350  wrdexb  14462  restid  17367  prdsbas  17391  prdsplusg  17392  prdsmulr  17393  prdsvsca  17394  prdshom  17401  sscpwex  17753  pmtrfv  19398  istopon  22873  tgval  22916  eltg2  22919  tgss2  22948  neiptoptop  23092  restin  23127  restntr  23143  cnprest2  23251  pnrmopn  23304  cnrmnrm  23322  cmpsublem  23360  cmpsub  23361  cmpcld  23363  hausmapdom  23461  isref  23470  locfindis  23491  txbasex  23527  dfac14lem  23578  xkopt  23616  xkopjcn  23617  qtopval2  23657  elqtop  23658  fbssfi  23798  ptcmplem2  24014  cnextfval  24023  tuslem  24227  madeval  27845  pliguhgr  30580  acunirnmpt2  32756  acunirnmpt2f  32757  ist0cld  34017  hasheuni  34269  insiga  34321  sigagenval  34324  omsval  34477  omssubadd  34484  sibfof  34524  sitmcl  34535  kur14  35438  cvmscld  35495  fobigcup  36120  hfuni  36406  isfne  36561  isfne4b  36563  fnemeet1  36588  tailfval  36594  bj-restuni2  37378  pibt2  37699  kelac2  43451  cnfex  45417  unidmex  45439  pwpwuni  45446  salgenval  46708  intsaluni  46716  salgenn0  46718  caragenunidm  46895  afv2ex  47603  iscnrm3rlem3  49330