This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfcr

Description: Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016) Drop ax-12 but use ax-8 , df-clel , and avoid a DV condition on y , A . (Revised by SN, 3-Jun-2024)

Ref Expression
Assertion nfcr 
|- ( F/_ x A -> F/ x y e. A )

Proof

Step Hyp Ref Expression
1 df-nfc 
 |-  ( F/_ x A <-> A. z F/ x z e. A )
2 eleq1w 
 |-  ( z = y -> ( z e. A <-> y e. A ) )
3 2 nfbidv 
 |-  ( z = y -> ( F/ x z e. A <-> F/ x y e. A ) )
4 3 spvv 
 |-  ( A. z F/ x z e. A -> F/ x y e. A )
5 1 4 sylbi 
 |-  ( F/_ x A -> F/ x y e. A )