Theorem wl-hbae1

Description: This specialization of hbae does not depend on ax-11 . (Contributed by Wolf Lammen, 8-Aug-2021)

	Ref	Expression
Assertion	wl-hbae1	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 ∀ 𝑥 𝑥 = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		axc11n	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 𝑦 = 𝑥 )
2		axc11n	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ∀ 𝑥 𝑥 = 𝑦 )
3	2	axc4i	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ∀ 𝑦 ∀ 𝑥 𝑥 = 𝑦 )
4	1 3	syl	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 ∀ 𝑥 𝑥 = 𝑦 )