Metamath Proof Explorer


Theorem bj-dvelimv

Description: A version of dvelim using the "nonfree" idiom. (Contributed by BJ, 20-Oct-2021) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-dvelimv.nf
|- F/ x ps
bj-dvelimv.is
|- ( z = y -> ( ps <-> ph ) )
Assertion bj-dvelimv
|- ( -. A. x x = y -> F/ x ph )

Proof

Step Hyp Ref Expression
1 bj-dvelimv.nf
 |-  F/ x ps
2 bj-dvelimv.is
 |-  ( z = y -> ( ps <-> ph ) )
3 1 a1i
 |-  ( T. -> F/ x ps )
4 3 2 bj-dvelimdv1
 |-  ( T. -> ( -. A. x x = y -> F/ x ph ) )
5 4 mptru
 |-  ( -. A. x x = y -> F/ x ph )