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

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 
|- ( ph -> A. x ph )
dvelimhw.2 
|- ( ps -> A. z ps )
dvelimhw.3 
|- ( z = y -> ( ph <-> ps ) )
dvelimhw.4 
|- ( -. A. x x = y -> ( y = z -> A. x y = z ) )
Assertion dvelimhw 
|- ( -. A. x x = y -> ( ps -> A. x ps ) )

Proof

Step Hyp Ref Expression
1 dvelimhw.1 
 |-  ( ph -> A. x ph )
2 dvelimhw.2 
 |-  ( ps -> A. z ps )
3 dvelimhw.3 
 |-  ( z = y -> ( ph <-> ps ) )
4 dvelimhw.4 
 |-  ( -. A. x x = y -> ( y = z -> A. x y = z ) )
5 nfv 
 |-  F/ z -. A. x x = y
6 equcom 
 |-  ( z = y <-> y = z )
7 nfna1 
 |-  F/ x -. A. x x = y
8 7 4 nf5d 
 |-  ( -. A. x x = y -> F/ x y = z )
9 6 8 nfxfrd 
 |-  ( -. A. x x = y -> F/ x z = y )
10 1 nf5i 
 |-  F/ x ph
11 10 a1i 
 |-  ( -. A. x x = y -> F/ x ph )
12 9 11 nfimd 
 |-  ( -. A. x x = y -> F/ x ( z = y -> ph ) )
13 5 12 nfald 
 |-  ( -. A. x x = y -> F/ x A. z ( z = y -> ph ) )
14 2 3 equsalhw 
 |-  ( A. z ( z = y -> ph ) <-> ps )
15 14 nfbii 
 |-  ( F/ x A. z ( z = y -> ph ) <-> F/ x ps )
16 13 15 sylib 
 |-  ( -. A. x x = y -> F/ x ps )
17 16 nf5rd 
 |-  ( -. A. x x = y -> ( ps -> A. x ps ) )