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

Theorem cbvalv 1955
 Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
cbvalv.1
Assertion
Ref Expression
cbvalv
Distinct variable groups:   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem cbvalv
StepHypRef Expression
1 nfv 1609 . 2
2 nfv 1609 . 2
3 cbvalv.1 . 2
41, 2, 3cbval 1937 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176  wal 1530 This theorem is referenced by:  ax10-16  2142  nfcjust  2420  cdeqal1  2995  zfpow  4205  tfisi  4665  pssnn  7097  findcard  7113  findcard3  7116  zfinf  7356  aceq0  7761  kmlem1  7792  kmlem13  7804  fin23lem32  7986  fin23lem41  7994  zfac  8102  zfcndpow  8254  zfcndinf  8256  zfcndac  8257  axgroth4  8470  ramcl  13092  mreexexlemd  13562  relexpindlem  24051  dfon2lem6  24215  dfon2lem7  24216  dfon2  24219  dfac11  27263  bnj1112  29329 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878 This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535
 Copyright terms: Public domain W3C validator