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	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
Assertion	ax12f	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax12f.1	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2		ax-1	⊢ ( 𝜑 → ( 𝑥 = 𝑦 → 𝜑 ) )
3	1 2	alrimih	⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
4	3	2a1i	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) )