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

Metamath Proof Explorer

Theorem dvelimf

Description: Version of dvelimv without any variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 1-Oct-2002) (Revised by Mario Carneiro, 6-Oct-2016) (Proof shortened by Wolf Lammen, 11-May-2018) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 dvelimf.1 ⊢ Ⅎ x φ
2 dvelimf.2 ⊢ Ⅎ z ψ
3 dvelimf.3 ⊢ z = y → φ ↔ ψ
4 2 3 equsal ⊢ ∀ z z = y → φ ↔ ψ
5 4 bicomi ⊢ ψ ↔ ∀ z z = y → φ
6 nfnae ⊢ Ⅎ z ¬ ∀ x x = y
7 nfeqf ⊢ ¬ ∀ x x = z ∧ ¬ ∀ x x = y → Ⅎ x z = y
8 7 ancoms ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x z = y
9 1 a1i ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x φ
10 8 9 nfimd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x z = y → φ
11 6 10 nfald2 ⊢ ¬ ∀ x x = y → Ⅎ x ∀ z z = y → φ
12 5 11 nfxfrd ⊢ ¬ ∀ x x = y → Ⅎ x ψ