MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uniexg Structured version   Visualization version   GIF version

Theorem uniexg 7682
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.
StepHypRef Expression
1 unieq 4881 . . 3 (𝑥 = 𝐴 𝑥 = 𝐴)
21eleq1d 2823 . 2 (𝑥 = 𝐴 → ( 𝑥 ∈ V ↔ 𝐴 ∈ V))
3 vuniex 7681 . 2 𝑥 ∈ V
42, 3vtoclg 3528 1 (𝐴𝑉 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  Vcvv 3448   cuni 4870
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5261  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932  df-uni 4871
This theorem is referenced by:  uniex  7683  uniexd  7684  abnexg  7695  uniexb  7703  pwexr  7704  ssonuni  7719  ssonprc  7727  dmexg  7845  rnexg  7846  undefval  8212  onovuni  8293  tz7.44lem1  8356  tz7.44-3  8359  en1unielOLD  8980  disjen  9085  domss2  9087  fival  9355  fipwuni  9369  supexd  9396  cantnflem1  9632  dfac8clem  9975  onssnum  9983  dfac12lem1  10086  dfac12lem2  10087  fin1a2lem12  10354  hsmexlem1  10369  wrdexb  14420  restid  17322  prdsbas  17346  prdsplusg  17347  prdsmulr  17348  prdsvsca  17349  prdshom  17356  sscpwex  17705  pmtrfv  19241  istopon  22277  tgval  22321  eltg2  22324  tgss2  22353  neiptoptop  22498  restin  22533  restntr  22549  cnprest2  22657  pnrmopn  22710  cnrmnrm  22728  cmpsublem  22766  cmpsub  22767  cmpcld  22769  hausmapdom  22867  isref  22876  locfindis  22897  txbasex  22933  dfac14lem  22984  xkopt  23022  xkopjcn  23023  qtopval2  23063  elqtop  23064  fbssfi  23204  ptcmplem2  23420  cnextfval  23429  tuslem  23634  tuslemOLD  23635  madeval  27204  pliguhgr  29470  acunirnmpt2  31618  acunirnmpt2f  31619  ist0cld  32454  hasheuni  32724  insiga  32776  sigagenval  32779  omsval  32933  omssubadd  32940  sibfof  32980  sitmcl  32991  kur14  33850  cvmscld  33907  fobigcup  34514  hfuni  34798  isfne  34840  isfne4b  34842  fnemeet1  34867  tailfval  34873  bj-restuni2  35598  pibt2  35917  imaexALTV  36820  kelac2  41421  cnfex  43307  unidmex  43332  pwpwuni  43339  salgenval  44636  intsaluni  44644  salgenn0  44646  caragenunidm  44823  afv2ex  45520  iscnrm3rlem3  47049
  Copyright terms: Public domain W3C validator