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 x ψ
bj-dvelimv.is z = y ψ φ
Assertion bj-dvelimv ¬ x x = y x φ

Proof

Step Hyp Ref Expression
1 bj-dvelimv.nf x ψ
2 bj-dvelimv.is z = y ψ φ
3 1 a1i x ψ
4 3 2 bj-dvelimdv1 ¬ x x = y x φ
5 4 mptru ¬ x x = y x φ