Theorem uniexg 7757

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 7756	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3517	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-uni 4867

This theorem is used by:  uniex  7758  uniexd  7759  abnexg  7770  uniexb  7778  pwexr  7779  ssonuni  7794  ssonprc  7801  dmexg  7913  rnexg  7914  undefval  8294  onovuni  8350  tz7.44lem1  8413  tz7.44-3  8416  disjen  9153  domss2  9155  fival  9404  fipwuni  9418  supexd  9445  cantnflem1  9690  hfuniOLD  9925  dfac8clem  10111  onssnum  10119  dfac12lem1  10222  dfac12lem2  10223  fin1a2lem12  10489  hsmexlem1  10504  wrdexb  14670  restid  17604  prdsbas  17628  prdsplusg  17629  prdsmulr  17630  prdsvsca  17631  prdshom  17638  sscpwex  17990  pmtrfv  19666  istopon  23230  tgval  23273  eltg2  23276  tgss2  23305  neiptoptop  23449  restin  23484  restntr  23500  cnprest2  23608  pnrmopn  23661  cnrmnrm  23679  cmpsublem  23717  cmpsub  23718  cmpcld  23720  hausmapdom  23819  isref  23828  locfindis  23849  txbasex  23885  dfac14lem  23936  xkopt  23974  xkopjcn  23975  qtopval2  24015  elqtop  24016  fbssfi  24156  ptcmplem2  24372  cnextfval  24381  tuslem  24585  madeval  28218  pliguhgr  31088  acunirnmpt2  33296  acunirnmpt2f  33297  ist0cld  34507  hasheuni  34759  insiga  34812  sigagenval  34815  omsval  34967  omssubadd  34974  sibfof  35014  sitmcl  35025  kur14  36023  cvmscld  36080  fobigcup  36704  isfne  37169  isfne4b  37171  fnemeet1  37196  tailfval  37202  bj-restuni2  38061  pibt2  38383  kelac2  44109  cnfex  46087  unidmex  46109  pwpwuni  46116  salgenval  47373  intsaluni  47381  salgenn0  47383  caragenunidm  47560  afv2ex  48326  iscnrm3rlem3  50092