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	$$⊢\underset{\_}{Ⅎ}xA\to Ⅎxy\in A$$

Proof

Step	Hyp	Ref	Expression
1		df-nfc	$$⊢\underset{\_}{Ⅎ}xA\leftrightarrow \forall zℲxz\in A$$
2		eleq1w	$$⊢z=y\to \left(z\in A\leftrightarrow y\in A\right)$$
3	2	nfbidv	$$⊢z=y\to \left(Ⅎxz\in A\leftrightarrow Ⅎxy\in A\right)$$
4	3	spvv	$$⊢\forall zℲxz\in A\to Ⅎxy\in A$$
5	1 4	sylbi	$$⊢\underset{\_}{Ⅎ}xA\to Ⅎxy\in A$$