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 
|- ( -. A. x x = y -> F/ x y e. z )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ x t e. z
2 elequ1 
 |-  ( t = y -> ( t e. z <-> y e. z ) )
3 1 2 bj-dvelimv 
 |-  ( -. A. x x = y -> F/ x y e. z )