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

Theorem cbvalv 2129
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 1769 . 2  |-  F/ y
ph
2 nfv 1769 . 2  |-  F/ x ps
3 cbvalv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbval 2127 1  |-  ( A. x ph  <->  A. y ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   A.wal 1450
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-nf 1676
This theorem is referenced by:  nfcjust  2600  cdeqal1  3246  zfpow  4580  tfisi  6704  pssnn  7808  findcard  7828  findcard3  7832  zfinf  8162  aceq0  8567  kmlem1  8598  kmlem13  8610  fin23lem32  8792  fin23lem41  8800  zfac  8908  zfcndpow  9059  zfcndinf  9061  zfcndac  9062  axgroth4  9275  relexpindlem  13203  ramcl  15066  mreexexlemd  15628  bnj1112  29864  dfon2lem6  30505  dfon2lem7  30506  dfon2  30509  phpreu  31993  axc11n-16  32573  dfac11  35991
  Copyright terms: Public domain W3C validator