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

Theorem cbvalv 2116
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 1761 . 2  |-  F/ y
ph
2 nfv 1761 . 2  |-  F/ x ps
3 cbvalv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbval 2114 1  |-  ( A. x ph  <->  A. y ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188   A.wal 1442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668
This theorem is referenced by:  nfcjust  2580  cdeqal1  3258  zfpow  4582  tfisi  6685  pssnn  7790  findcard  7810  findcard3  7814  zfinf  8144  aceq0  8549  kmlem1  8580  kmlem13  8592  fin23lem32  8774  fin23lem41  8782  zfac  8890  zfcndpow  9041  zfcndinf  9043  zfcndac  9044  axgroth4  9257  relexpindlem  13126  ramcl  14987  mreexexlemd  15550  bnj1112  29792  dfon2lem6  30434  dfon2lem7  30435  dfon2  30438  phpreu  31929  axc11n-16  32509  dfac11  35920
  Copyright terms: Public domain W3C validator