Metamath Proof Explorer


Theorem bj-nfeel2

Description: Nonfreeness in a membership statement. (Contributed by BJ, 20-Oct-2021) (Proof modification is discouraged.)

Ref Expression
Assertion bj-nfeel2 ¬ x x = y x y z

Proof

Step Hyp Ref Expression
1 nfv x t z
2 elequ1 t = y t z y z
3 1 2 bj-dvelimv ¬ x x = y x y z