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	$$⊢\forall xx=y\to \forall y\forall xx=y$$

Proof

Step	Hyp	Ref	Expression
1		axc11n	$$⊢\forall xx=y\to \forall yy=x$$
2		axc11n	$$⊢\forall yy=x\to \forall xx=y$$
3	2	axc4i	$$⊢\forall yy=x\to \forall y\forall xx=y$$
4	1 3	syl	$$⊢\forall xx=y\to \forall y\forall xx=y$$