Theorem bj-nfcf

Description: Version of df-nfc with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 2-May-2019)

	Ref	Expression
Hypothesis	bj-nfcf.nf	$$⊢\underset{\_}{Ⅎ}yA$$
Assertion	bj-nfcf	$$⊢\underset{\_}{Ⅎ}xA\leftrightarrow \forall yℲxy\in A$$

Proof

Step	Hyp	Ref	Expression
1		bj-nfcf.nf	$$⊢\underset{\_}{Ⅎ}yA$$
2		df-nfc	$$⊢\underset{\_}{Ⅎ}xA\leftrightarrow \forall zℲxz\in A$$
3	1	nfcri	$$⊢Ⅎyz\in A$$
4	3	nfnf	$$⊢ℲyℲxz\in A$$
5	4	sb8v	$$⊢\forall zℲxz\in A\leftrightarrow \forall y\left[y/z\right]Ⅎxz\in A$$
6		bj-sbnf	$$⊢\left[y/z\right]Ⅎxz\in A\leftrightarrow Ⅎx\left[y/z\right]z\in A$$
7		clelsb1	$$⊢\left[y/z\right]z\in A\leftrightarrow y\in A$$
8	7	nfbii	$$⊢Ⅎx\left[y/z\right]z\in A\leftrightarrow Ⅎxy\in A$$
9	6 8	bitri	$$⊢\left[y/z\right]Ⅎxz\in A\leftrightarrow Ⅎxy\in A$$
10	9	albii	$$⊢\forall y\left[y/z\right]Ⅎxz\in A\leftrightarrow \forall yℲxy\in A$$
11	5 10	bitri	$$⊢\forall zℲxz\in A\leftrightarrow \forall yℲxy\in A$$
12	2 11	bitri	$$⊢\underset{\_}{Ⅎ}xA\leftrightarrow \forall yℲxy\in A$$