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	|- F/_ y A
Assertion	bj-nfcf	|- ( F/_ x A <-> A. y F/ x y e. A )

Proof

Step	Hyp	Ref	Expression
1		bj-nfcf.nf	|- F/_ y A
2		df-nfc	|- ( F/_ x A <-> A. z F/ x z e. A )
3	1	nfcri	|- F/ y z e. A
4	3	nfnf	|- F/ y F/ x z e. A
5	4	sb8v	|- ( A. z F/ x z e. A <-> A. y [ y / z ] F/ x z e. A )
6		bj-sbnf	|- ( [ y / z ] F/ x z e. A <-> F/ x [ y / z ] z e. A )
7		clelsb1	|- ( [ y / z ] z e. A <-> y e. A )
8	7	nfbii	|- ( F/ x [ y / z ] z e. A <-> F/ x y e. A )
9	6 8	bitri	|- ( [ y / z ] F/ x z e. A <-> F/ x y e. A )
10	9	albii	|- ( A. y [ y / z ] F/ x z e. A <-> A. y F/ x y e. A )
11	5 10	bitri	|- ( A. z F/ x z e. A <-> A. y F/ x y e. A )
12	2 11	bitri	|- ( F/_ x A <-> A. y F/ x y e. A )