Theorem ax12f

Description: Basis step for constructing a substitution instance of ax-c15 without using ax-c15 . We can start with any formula ph in which x is not free. (Contributed by NM, 21-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ax12f.1	$$⊢\phi \to \forall x\phi$$
2		ax-1	$$⊢\phi \to \left(x=y\to \phi \right)$$
3	1 2	alrimih	$$⊢\phi \to \forall x\left(x=y\to \phi \right)$$
4	3	2a1i	$$⊢\neg \forall xx=y\to \left(x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)$$