Metamath Proof Explorer


Theorem cbvalivw

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. Part of Lemma 7 of KalishMontague p. 86. (Contributed by NM, 9-Apr-2017)

Ref Expression
Hypothesis cbvalivw.1
|- ( x = y -> ( ph -> ps ) )
Assertion cbvalivw
|- ( A. x ph -> A. y ps )

Proof

Step Hyp Ref Expression
1 cbvalivw.1
 |-  ( x = y -> ( ph -> ps ) )
2 1 spimvw
 |-  ( A. x ph -> ps )
3 2 alrimiv
 |-  ( A. x ph -> A. y ps )