Theorem uniexg 7687

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3441  ∪ cuni 4864

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 5242  ax-un 7682

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 3443  df-ss 3919  df-uni 4865

This theorem is referenced by:  uniex  7688  uniexd  7689  abnexg  7703  uniexb  7711  pwexr  7712  ssonuni  7727  ssonprc  7734  dmexg  7845  rnexg  7846  undefval  8220  onovuni  8276  tz7.44lem1  8338  tz7.44-3  8341  disjen  9066  domss2  9068  fival  9319  fipwuni  9333  supexd  9360  cantnflem1  9602  dfac8clem  9946  onssnum  9954  dfac12lem1  10058  dfac12lem2  10059  fin1a2lem12  10325  hsmexlem1  10340  wrdexb  14452  restid  17357  prdsbas  17381  prdsplusg  17382  prdsmulr  17383  prdsvsca  17384  prdshom  17391  sscpwex  17743  pmtrfv  19385  istopon  22860  tgval  22903  eltg2  22906  tgss2  22935  neiptoptop  23079  restin  23114  restntr  23130  cnprest2  23238  pnrmopn  23291  cnrmnrm  23309  cmpsublem  23347  cmpsub  23348  cmpcld  23350  hausmapdom  23448  isref  23457  locfindis  23478  txbasex  23514  dfac14lem  23565  xkopt  23603  xkopjcn  23604  qtopval2  23644  elqtop  23645  fbssfi  23785  ptcmplem2  24001  cnextfval  24010  tuslem  24214  madeval  27832  pliguhgr  30565  acunirnmpt2  32741  acunirnmpt2f  32742  ist0cld  33992  hasheuni  34244  insiga  34296  sigagenval  34299  omsval  34452  omssubadd  34459  sibfof  34499  sitmcl  34510  kur14  35412  cvmscld  35469  fobigcup  36094  hfuni  36380  isfne  36535  isfne4b  36537  fnemeet1  36562  tailfval  36568  bj-restuni2  37305  pibt2  37624  kelac2  43374  cnfex  45340  unidmex  45362  pwpwuni  45369  salgenval  46632  intsaluni  46640  salgenn0  46642  caragenunidm  46819  afv2ex  47527  iscnrm3rlem3  49254