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

Theorem cbvalv 1972
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 1674 . 2  |-  F/ y
ph
2 nfv 1674 . 2  |-  F/ x ps
3 cbvalv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbval 1970 1  |-  ( A. x ph  <->  A. y ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591
This theorem is referenced by:  axc11n-16  2245  nfcjust  2597  cdeqal1  3261  zfpow  4555  tfisi  6555  pssnn  7618  findcard  7638  findcard3  7642  zfinf  7932  aceq0  8375  kmlem1  8406  kmlem13  8418  fin23lem32  8600  fin23lem41  8608  zfac  8716  zfcndpow  8870  zfcndinf  8872  zfcndac  8873  axgroth4  9086  ramcl  14178  mreexexlemd  14670  relexpindlem  27461  dfon2lem6  27721  dfon2lem7  27722  dfon2  27725  dfac11  29539  bnj1112  32256
  Copyright terms: Public domain W3C validator