Theorem uniexg 7593

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 4850	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2823	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V))
3		vuniex 7592	. 2 ⊢ ∪ 𝑥 ∈ V
4	2, 3	vtoclg 3505	1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  Vcvv 3432  ∪ cuni 4839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840

This theorem is referenced by:  uniex  7594  uniexd  7595  abnexg  7606  uniexb  7614  pwexr  7615  ssonuni  7630  ssonprc  7637  dmexg  7750  rnexg  7751  undefval  8092  onovuni  8173  tz7.44lem1  8236  tz7.44-3  8239  en1unielOLD  8819  disjen  8921  domss2  8923  fival  9171  fipwuni  9185  supexd  9212  cantnflem1  9447  dfac8clem  9788  onssnum  9796  dfac12lem1  9899  dfac12lem2  9900  fin1a2lem12  10167  hsmexlem1  10182  wrdexb  14228  restid  17144  prdsbas  17168  prdsplusg  17169  prdsmulr  17170  prdsvsca  17171  prdshom  17178  sscpwex  17527  pmtrfv  19060  istopon  22061  tgval  22105  eltg2  22108  tgss2  22137  neiptoptop  22282  restin  22317  restntr  22333  cnprest2  22441  pnrmopn  22494  cnrmnrm  22512  cmpsublem  22550  cmpsub  22551  cmpcld  22553  hausmapdom  22651  isref  22660  locfindis  22681  txbasex  22717  dfac14lem  22768  xkopt  22806  xkopjcn  22807  qtopval2  22847  elqtop  22848  fbssfi  22988  ptcmplem2  23204  cnextfval  23213  tuslem  23418  tuslemOLD  23419  pliguhgr  28848  acunirnmpt2  30997  acunirnmpt2f  30998  ist0cld  31783  hasheuni  32053  insiga  32105  sigagenval  32108  omsval  32260  omssubadd  32267  sibfof  32307  sitmcl  32318  kur14  33178  cvmscld  33235  madeval  34036  fobigcup  34202  hfuni  34486  isfne  34528  isfne4b  34530  fnemeet1  34555  tailfval  34561  bj-restuni2  35269  pibt2  35588  imaexALTV  36465  kelac2  40890  cnfex  42571  unidmex  42598  pwpwuni  42605  salgenval  43862  intsaluni  43868  salgenn0  43870  caragenunidm  44046  afv2ex  44706  iscnrm3rlem3  46236