Theorem cbvaev

Description: Change bound variable in an equality with a disjoint variable condition. Instance of aev . (Contributed by NM, 22-Jul-2015) (Revised by BJ, 18-Jun-2019)

	Ref	Expression
Assertion	cbvaev	$$⊢\forall xx=y\to \forall zz=y$$

Proof

Step	Hyp	Ref	Expression
1		ax7	$$⊢x=t\to \left(x=y\to t=y\right)$$
2	1	cbvalivw	$$⊢\forall xx=y\to \forall tt=y$$
3		ax7	$$⊢t=z\to \left(t=y\to z=y\right)$$
4	3	cbvalivw	$$⊢\forall tt=y\to \forall zz=y$$
5	2 4	syl	$$⊢\forall xx=y\to \forall zz=y$$