Theorem axc11-o

Description: Show that ax-c11 can be derived from ax-c11n and ax-12 . An open problem is whether this theorem can be derived from ax-c11n and the others when ax-12 is replaced with ax-c15 or ax12v . See Theorems axc11nfromc11 for the rederivation of ax-c11n from axc11 .

Normally, axc11 should be used rather than ax-c11 or axc11-o , except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	axc11-o	$$⊢\forall xx=y\to \left(\forall x\phi \to \forall y\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-c11n	$$⊢\forall xx=y\to \forall yy=x$$
2		ax12	$$⊢y=x\to \left(\forall x\phi \to \forall y\left(y=x\to \phi \right)\right)$$
3	2	equcoms	$$⊢x=y\to \left(\forall x\phi \to \forall y\left(y=x\to \phi \right)\right)$$
4	3	sps-o	$$⊢\forall xx=y\to \left(\forall x\phi \to \forall y\left(y=x\to \phi \right)\right)$$
5		pm2.27	$$⊢y=x\to \left(\left(y=x\to \phi \right)\to \phi \right)$$
6	5	al2imi	$$⊢\forall yy=x\to \left(\forall y\left(y=x\to \phi \right)\to \forall y\phi \right)$$
7	1 4 6	sylsyld	$$⊢\forall xx=y\to \left(\forall x\phi \to \forall y\phi \right)$$