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φψ
Assertion cbvalivw xφyψ

Proof

Step Hyp Ref Expression
1 cbvalivw.1 x=yφψ
2 1 spimvw xφψ
3 2 alrimiv xφyψ