This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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