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

Proof

Step	Hyp	Ref	Expression
1		ax12inda2.1	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) )
2		ax-1	⊢ ( ∀ 𝑧 𝜑 → ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) )
3		axc16g-o	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) )
4	2 3	syl5	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) )
5	4	a1d	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( 𝑥 = 𝑦 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) ) )
6	5	a1d	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) ) ) )
7	1	ax12indalem	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) ) ) )
8	6 7	pm2.61i	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ∀ 𝑧 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑧 𝜑 ) ) ) )