Metamath Proof Explorer


Theorem wl-cbvmotv

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. Part of Lemma 7 of KalishMontague p. 86. (Contributed by Wolf Lammen, 5-Mar-2023)

Ref Expression
Assertion wl-cbvmotv *x*y

Proof

Step Hyp Ref Expression
1 ax7v2 x=yx=zy=z
2 1 imim2d x=yx=zy=z
3 2 cbvalivw xx=zyy=z
4 3 eximi zxx=zzyy=z
5 df-mo *xzxx=z
6 df-mo *yzyy=z
7 4 5 6 3imtr4i *x*y