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	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 𝑧 = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		ax7	⊢ ( 𝑥 = 𝑡 → ( 𝑥 = 𝑦 → 𝑡 = 𝑦 ) )
2	1	cbvalivw	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑡 𝑡 = 𝑦 )
3		ax7	⊢ ( 𝑡 = 𝑧 → ( 𝑡 = 𝑦 → 𝑧 = 𝑦 ) )
4	3	cbvalivw	⊢ ( ∀ 𝑡 𝑡 = 𝑦 → ∀ 𝑧 𝑧 = 𝑦 )
5	2 4	syl	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 𝑧 = 𝑦 )