Theorem wl-axc11rc11

Description: Proving axc11r from axc11 . The hypotheses are two instances of axc11 used in the proof here. Some systems introduce axc11 as an axiom, see for example System S2 in https://us.metamath.org/downloads/finiteaxiom.pdf .

By contrast, this database sees the variant axc11r , directly derived from ax-12 , as foundational. Later axc11 is proven somewhat trickily, requiring ax-10 and ax-13 , see its proof. (Contributed by Wolf Lammen, 18-Jul-2023)

	Ref	Expression
Hypotheses	wl-axc11rc11.1	$$⊢\forall yy=x\to \left(\forall yy=x\to \forall xy=x\right)$$
	wl-axc11rc11.2	$$⊢\forall xx=y\to \left(\forall x\phi \to \forall y\phi \right)$$
Assertion	wl-axc11rc11	$$⊢\forall yy=x\to \left(\forall x\phi \to \forall y\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		wl-axc11rc11.1	$$⊢\forall yy=x\to \left(\forall yy=x\to \forall xy=x\right)$$
2		wl-axc11rc11.2	$$⊢\forall xx=y\to \left(\forall x\phi \to \forall y\phi \right)$$
3	1	pm2.43i	$$⊢\forall yy=x\to \forall xy=x$$
4		equcomi	$$⊢y=x\to x=y$$
5	4	alimi	$$⊢\forall xy=x\to \forall xx=y$$
6	3 5 2	3syl	$$⊢\forall yy=x\to \left(\forall x\phi \to \forall y\phi \right)$$