MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vtoclga Unicode version

Theorem vtoclga 3173
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.)
Hypotheses
Ref Expression
vtoclga.1
vtoclga.2
Assertion
Ref Expression
vtoclga
Distinct variable groups:   ,   ,   ,

Proof of Theorem vtoclga
StepHypRef Expression
1 nfcv 2619 . 2
2 nfv 1707 . 2
3 vtoclga.1 . 2
4 vtoclga.2 . 2
51, 2, 3, 4vtoclgaf 3172 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818
This theorem is referenced by:  vtoclri  3184  ssuni  4271  disjxiun  4449  opabiota  5936  fvmpt3  5959  fvmptss  5964  fnressn  6083  fressnfv  6085  caovord  6486  caovmo  6512  ordunisuc  6667  tfis3  6692  onfununi  7031  smogt  7057  tz7.44-1  7091  tz7.44-2  7092  tz7.44-3  7093  nnacl  7279  nnmcl  7280  nnecl  7281  nnacom  7285  nnaass  7290  nndi  7291  nnmass  7292  nnmsucr  7293  nnmcom  7294  nnmordi  7299  ixpfn  7495  findcard  7779  findcard2  7780  marypha1  7914  cantnfle  8111  cantnflem1  8129  cantnfleOLD  8141  cantnflem1OLD  8152  cnfcom  8165  cnfcomOLD  8173  fseqenlem1  8426  ackbij1lem5  8625  ackbij1lem8  8628  cardcf  8653  cfsmolem  8671  wunex2  9137  ingru  9214  recrecnq  9366  prlem934  9432  nn1suc  10582  uzind4s2  11171  rpnnen1  11242  cnref1o  11244  xmulasslem  11506  om2uzsuci  12059  expcl2lem  12178  hashmap  12493  hashpw  12494  seqcoll  12512  climub  13484  climserle  13485  sumrblem  13533  fsumcvg  13534  summolem2a  13537  infcvgaux2i  13669  prodfn0  13703  prodfrec  13704  prodrblem  13736  fprodcvg  13737  prodmolem2a  13741  divalglem8  14058  bezoutlem1  14176  alginv  14204  algcvg  14205  algcvga  14208  algfx  14209  isprm2lem  14224  prmind2  14228  prmpwdvds  14422  cnextfvval  20565  xrsxmet  21314  xrhmeo  21446  cmetcaulem  21727  bcth3  21770  itg2addlem  22165  taylfval  22754  sinord  22921  logexprlim  23500  lgsdir2lem4  23601  hlim2  26109  elnlfn  26847  lnconi  26952  chirredlem3  27311  chirredlem4  27312  cnre2csqlem  27892  eulerpartlemsf  28298  eulerpartlemn  28320  subfacp1lem1  28623  wfis3  29295  frins3  29331  wfr2  29360  findreccl  29918  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  ftc1anclem3  30092  ftc1anclem8  30097  nn0prpwlem  30140  sdclem2  30235  iscringd  30396  zindbi  30882  fmuldfeq  31577  sumnnodd  31636  iblspltprt  31772  stoweidlem2  31784  stoweidlem17  31799  stoweidlem21  31803  stoweidlem43  31825  stoweidlem51  31833  wallispi  31852  bnj1321  34083  bnj1418  34096  renegclALT  34694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111
  Copyright terms: Public domain W3C validator