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

Proof

Step Hyp Ref Expression
1 dvelimh.1
 |-  ( ph -> A. x ph )
2 dvelimh.2
 |-  ( ps -> A. z ps )
3 dvelimh.3
 |-  ( z = y -> ( ph <-> ps ) )
4 1 nf5i
 |-  F/ x ph
5 2 nf5i
 |-  F/ z ps
6 4 5 3 dvelimf
 |-  ( -. A. x x = y -> F/ x ps )
7 6 nf5rd
 |-  ( -. A. x x = y -> ( ps -> A. x ps ) )