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 ψ