Theorem ax12inda2

Description: Induction step for constructing a substitution instance of ax-c15 without using ax-c15 . Quantification case. When z and y are distinct, this theorem avoids the dummy variables needed by the more general ax12inda . (Contributed by NM, 24-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ax12inda2.1	$$⊢\neg \forall xx=y\to \left(x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)$$
Assertion	ax12inda2	$$⊢\neg \forall xx=y\to \left(x=y\to \left(\forall z\phi \to \forall x\left(x=y\to \forall z\phi \right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax12inda2.1	$$⊢\neg \forall xx=y\to \left(x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)$$
2		ax-1	$$⊢\forall z\phi \to \left(x=y\to \forall z\phi \right)$$
3		axc16g-o	$$⊢\forall yy=z\to \left(\left(x=y\to \forall z\phi \right)\to \forall x\left(x=y\to \forall z\phi \right)\right)$$
4	2 3	syl5	$$⊢\forall yy=z\to \left(\forall z\phi \to \forall x\left(x=y\to \forall z\phi \right)\right)$$
5	4	a1d	$$⊢\forall yy=z\to \left(x=y\to \left(\forall z\phi \to \forall x\left(x=y\to \forall z\phi \right)\right)\right)$$
6	5	a1d	$$⊢\forall yy=z\to \left(\neg \forall xx=y\to \left(x=y\to \left(\forall z\phi \to \forall x\left(x=y\to \forall z\phi \right)\right)\right)\right)$$
7	1	ax12indalem	$$⊢\neg \forall yy=z\to \left(\neg \forall xx=y\to \left(x=y\to \left(\forall z\phi \to \forall x\left(x=y\to \forall z\phi \right)\right)\right)\right)$$
8	6 7	pm2.61i	$$⊢\neg \forall xx=y\to \left(x=y\to \left(\forall z\phi \to \forall x\left(x=y\to \forall z\phi \right)\right)\right)$$