Theorem nfcr

Description: Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016) Drop ax-12 but use ax-8 , 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 )