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

Theorem cbvalv 1996
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 1683 . 2  |-  F/ y
ph
2 nfv 1683 . 2  |-  F/ x ps
3 cbvalv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbval 1994 1  |-  ( A. x ph  <->  A. y ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600
This theorem is referenced by:  axc11n-16  2261  nfcjust  2616  cdeqal1  3322  zfpow  4626  tfisi  6671  pssnn  7735  findcard  7755  findcard3  7759  zfinf  8052  aceq0  8495  kmlem1  8526  kmlem13  8538  fin23lem32  8720  fin23lem41  8728  zfac  8836  zfcndpow  8990  zfcndinf  8992  zfcndac  8993  axgroth4  9206  ramcl  14402  mreexexlemd  14895  relexpindlem  28537  dfon2lem6  28797  dfon2lem7  28798  dfon2  28801  dfac11  30612  bnj1112  33118
  Copyright terms: Public domain W3C validator