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

Metamath Proof Explorer

Theorem dvelimf-o

Description: Proof of dvelimh that uses ax-c11 but not ax-c15 , ax-c11n , or ax-12 . Version of dvelimh using ax-c11 instead of axc11 . (Contributed by NM, 12-Nov-2002) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses dvelimf-o.1 ⊢ φ → ∀ x φ
dvelimf-o.2 ⊢ ψ → ∀ z ψ
dvelimf-o.3 ⊢ z = y → φ ↔ ψ
Assertion dvelimf-o ⊢ ¬ ∀ x x = y → ψ → ∀ x ψ

Proof

Step Hyp Ref Expression
1 dvelimf-o.1 ⊢ φ → ∀ x φ
2 dvelimf-o.2 ⊢ ψ → ∀ z ψ
3 dvelimf-o.3 ⊢ z = y → φ ↔ ψ
4 hba1-o ⊢ ∀ z z = y → φ → ∀ z ∀ z z = y → φ
5 ax-c11 ⊢ ∀ z z = x → ∀ z ∀ z z = y → φ → ∀ x ∀ z z = y → φ
6 5 aecoms-o ⊢ ∀ x x = z → ∀ z ∀ z z = y → φ → ∀ x ∀ z z = y → φ
7 4 6 syl5 ⊢ ∀ x x = z → ∀ z z = y → φ → ∀ x ∀ z z = y → φ
8 7 a1d ⊢ ∀ x x = z → ¬ ∀ x x = y → ∀ z z = y → φ → ∀ x ∀ z z = y → φ
9 hbnae-o ⊢ ¬ ∀ x x = z → ∀ z ¬ ∀ x x = z
10 hbnae-o ⊢ ¬ ∀ x x = y → ∀ z ¬ ∀ x x = y
11 9 10 hban ⊢ ¬ ∀ x x = z ∧ ¬ ∀ x x = y → ∀ z ¬ ∀ x x = z ∧ ¬ ∀ x x = y
12 hbnae-o ⊢ ¬ ∀ x x = z → ∀ x ¬ ∀ x x = z
13 hbnae-o ⊢ ¬ ∀ x x = y → ∀ x ¬ ∀ x x = y
14 12 13 hban ⊢ ¬ ∀ x x = z ∧ ¬ ∀ x x = y → ∀ x ¬ ∀ x x = z ∧ ¬ ∀ x x = y
15 ax-c9 ⊢ ¬ ∀ x x = z → ¬ ∀ x x = y → z = y → ∀ x z = y
16 15 imp ⊢ ¬ ∀ x x = z ∧ ¬ ∀ x x = y → z = y → ∀ x z = y
17 1 a1i ⊢ ¬ ∀ x x = z ∧ ¬ ∀ x x = y → φ → ∀ x φ
18 14 16 17 hbimd ⊢ ¬ ∀ x x = z ∧ ¬ ∀ x x = y → z = y → φ → ∀ x z = y → φ
19 11 18 hbald ⊢ ¬ ∀ x x = z ∧ ¬ ∀ x x = y → ∀ z z = y → φ → ∀ x ∀ z z = y → φ
20 19 ex ⊢ ¬ ∀ x x = z → ¬ ∀ x x = y → ∀ z z = y → φ → ∀ x ∀ z z = y → φ
21 8 20 pm2.61i ⊢ ¬ ∀ x x = y → ∀ z z = y → φ → ∀ x ∀ z z = y → φ
22 2 3 equsalh ⊢ ∀ z z = y → φ ↔ ψ
23 22 albii ⊢ ∀ x ∀ z z = y → φ ↔ ∀ x ψ
24 21 22 23 3imtr3g ⊢ ¬ ∀ x x = y → ψ → ∀ x ψ