MPE Home 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  |-  ( 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 1609 . 2  |-  F/ y
ph
2 nfv 1609 . 2  |-  F/ x ps
3 cbvalv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbval 1937 1  |-  ( A. x ph  <->  A. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.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