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

Theorem cbvabv 2600
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-May-1999.)
Hypothesis
Ref Expression
cbvabv.1
Assertion
Ref Expression
cbvabv
Distinct variable groups:   ,   ,

Proof of Theorem cbvabv
StepHypRef Expression
1 nfv 1707 . 2
2 nfv 1707 . 2
3 cbvabv.1 . 2
41, 2, 3cbvab 2598 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  {cab 2442
This theorem is referenced by:  cdeqab1  3319  difjust  3477  unjust  3479  injust  3481  uniiunlem  3587  dfif3  3955  pwjust  4013  snjust  4028  intab  4317  intabs  4613  iotajust  5555  sbth  7657  cardprc  8382  iunfictbso  8516  aceq3lem  8522  isf33lem  8767  axdc3  8855  axdclem  8920  axdc  8922  genpv  9398  ltexpri  9442  recexpr  9450  supsr  9510  hashf1lem2  12505  mertens  13695  4sq  14482  nbgraf1olem5  24445  dispcmp  27862  eulerpart  28321  ballotlemfmpn  28433  subfacp1lem6  28629  subfacp1  28630  dfon2lem3  29217  dfon2lem7  29221  wfrlem1  29343  frrlem1  29387  ismblfin  30055  eldioph3  30699  diophrex  30709  ssfiunibd  31509  isuhgr  32366  isushgr  32367  bnj66  33918  bnj1234  34069  glbconxN  35102
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-or 370  df-an 371  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449
  Copyright terms: Public domain W3C validator