Theorem uniexg 7719

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 4885	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2814	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7718	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3523	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3450  ∪ cuni 4874

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 2702  ax-sep 5254  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-uni 4875

This theorem is referenced by:  uniex  7720  uniexd  7721  abnexg  7735  uniexb  7743  pwexr  7744  ssonuni  7759  ssonprc  7766  dmexg  7880  rnexg  7881  undefval  8258  onovuni  8314  tz7.44lem1  8376  tz7.44-3  8379  disjen  9104  domss2  9106  fival  9370  fipwuni  9384  supexd  9411  cantnflem1  9649  dfac8clem  9992  onssnum  10000  dfac12lem1  10104  dfac12lem2  10105  fin1a2lem12  10371  hsmexlem1  10386  wrdexb  14497  restid  17403  prdsbas  17427  prdsplusg  17428  prdsmulr  17429  prdsvsca  17430  prdshom  17437  sscpwex  17784  pmtrfv  19389  istopon  22806  tgval  22849  eltg2  22852  tgss2  22881  neiptoptop  23025  restin  23060  restntr  23076  cnprest2  23184  pnrmopn  23237  cnrmnrm  23255  cmpsublem  23293  cmpsub  23294  cmpcld  23296  hausmapdom  23394  isref  23403  locfindis  23424  txbasex  23460  dfac14lem  23511  xkopt  23549  xkopjcn  23550  qtopval2  23590  elqtop  23591  fbssfi  23731  ptcmplem2  23947  cnextfval  23956  tuslem  24161  madeval  27767  pliguhgr  30422  acunirnmpt2  32591  acunirnmpt2f  32592  ist0cld  33830  hasheuni  34082  insiga  34134  sigagenval  34137  omsval  34291  omssubadd  34298  sibfof  34338  sitmcl  34349  kur14  35210  cvmscld  35267  fobigcup  35895  hfuni  36179  isfne  36334  isfne4b  36336  fnemeet1  36361  tailfval  36367  bj-restuni2  37093  pibt2  37412  kelac2  43061  cnfex  45029  unidmex  45051  pwpwuni  45058  salgenval  46326  intsaluni  46334  salgenn0  46336  caragenunidm  46513  afv2ex  47219  iscnrm3rlem3  48934