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

Theorem cbvalv 2028
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 1712 . 2  |-  F/ y
ph
2 nfv 1712 . 2  |-  F/ x ps
3 cbvalv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbval 2026 1  |-  ( A. x ph  <->  A. y ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1396
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-nf 1622
This theorem is referenced by:  axc11n-16  2270  nfcjust  2603  cdeqal1  3315  zfpow  4616  tfisi  6666  pssnn  7731  findcard  7751  findcard3  7755  zfinf  8047  aceq0  8490  kmlem1  8521  kmlem13  8533  fin23lem32  8715  fin23lem41  8723  zfac  8831  zfcndpow  8983  zfcndinf  8985  zfcndac  8986  axgroth4  9199  relexpindlem  12981  ramcl  14634  mreexexlemd  15136  dfon2lem6  29463  dfon2lem7  29464  dfon2  29467  dfac11  31250  bnj1112  34459
  Copyright terms: Public domain W3C validator