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

Metamath Proof Explorer

Theorem dvelimh

Description: Version of dvelim without any variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 . Check out dvelimhw for a version requiring fewer axioms. (Contributed by NM, 1-Oct-2002) (Proof shortened by Wolf Lammen, 11-May-2018) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 dvelimh.1 ⊢ φ → ∀ x φ
2 dvelimh.2 ⊢ ψ → ∀ z ψ
3 dvelimh.3 ⊢ z = y → φ ↔ ψ
4 1 nf5i ⊢ Ⅎ x φ
5 2 nf5i ⊢ Ⅎ z ψ
6 4 5 3 dvelimf ⊢ ¬ ∀ x x = y → Ⅎ x ψ
7 6 nf5rd ⊢ ¬ ∀ x x = y → ψ → ∀ x ψ