Metamath Proof Explorer


Theorem dvelimhw

Description: Proof of dvelimh without using ax-13 but with additional distinct variable conditions. (Contributed by NM, 1-Oct-2002) (Revised by Andrew Salmon, 21-Jul-2011) (Revised by NM, 1-Aug-2017) (Proof shortened by Wolf Lammen, 23-Dec-2018)

Ref Expression
Hypotheses dvelimhw.1 φxφ
dvelimhw.2 ψzψ
dvelimhw.3 z=yφψ
dvelimhw.4 ¬xx=yy=zxy=z
Assertion dvelimhw ¬xx=yψxψ

Proof

Step Hyp Ref Expression
1 dvelimhw.1 φxφ
2 dvelimhw.2 ψzψ
3 dvelimhw.3 z=yφψ
4 dvelimhw.4 ¬xx=yy=zxy=z
5 nfv z¬xx=y
6 equcom z=yy=z
7 nfna1 x¬xx=y
8 7 4 nf5d ¬xx=yxy=z
9 6 8 nfxfrd ¬xx=yxz=y
10 1 nf5i xφ
11 10 a1i ¬xx=yxφ
12 9 11 nfimd ¬xx=yxz=yφ
13 5 12 nfald ¬xx=yxzz=yφ
14 2 3 equsalhw zz=yφψ
15 14 nfbii xzz=yφxψ
16 13 15 sylib ¬xx=yxψ
17 16 nf5rd ¬xx=yψxψ