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

Theorem cbvalv 1985
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
cbvalv.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvalv  |-  ( A. x ph  <->  A. y ps )
Distinct variable groups:    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem cbvalv
StepHypRef Expression
1 nfv 1630 . 2  |-  F/ y
ph
2 nfv 1630 . 2  |-  F/ x ps
3 cbvalv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbval 1983 1  |-  ( A. x ph  <->  A. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   A.wal 1550
This theorem is referenced by:  ax10-16  2268  nfcjust  2561  cdeqal1  3153  zfpow  4379  tfisi  4839  pssnn  7328  findcard  7348  findcard3  7351  zfinf  7595  aceq0  8000  kmlem1  8031  kmlem13  8043  fin23lem32  8225  fin23lem41  8233  zfac  8341  zfcndpow  8492  zfcndinf  8494  zfcndac  8495  axgroth4  8708  ramcl  13398  mreexexlemd  13870  relexpindlem  25140  dfon2lem6  25416  dfon2lem7  25417  dfon2  25420  dfac11  27138  bnj1112  29353
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator