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 ⊢ ¬ ∀ x x = y → x = y → φ → ∀ x x = y → φ
Assertion ax12inda2 ⊢ ¬ ∀ x x = y → x = y → ∀ z φ → ∀ x x = y → ∀ z φ

Proof

Step Hyp Ref Expression
1 ax12inda2.1 ⊢ ¬ ∀ x x = y → x = y → φ → ∀ x x = y → φ
2 ax-1 ⊢ ∀ z φ → x = y → ∀ z φ
3 axc16g-o ⊢ ∀ y y = z → x = y → ∀ z φ → ∀ x x = y → ∀ z φ
4 2 3 syl5 ⊢ ∀ y y = z → ∀ z φ → ∀ x x = y → ∀ z φ
5 4 a1d ⊢ ∀ y y = z → x = y → ∀ z φ → ∀ x x = y → ∀ z φ
6 5 a1d ⊢ ∀ y y = z → ¬ ∀ x x = y → x = y → ∀ z φ → ∀ x x = y → ∀ z φ
7 1 ax12indalem ⊢ ¬ ∀ y y = z → ¬ ∀ x x = y → x = y → ∀ z φ → ∀ x x = y → ∀ z φ
8 6 7 pm2.61i ⊢ ¬ ∀ x x = y → x = y → ∀ z φ → ∀ x x = y → ∀ z φ