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 ) |
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 ) |