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	⊢ Ⅎ 𝑦 𝐴
Assertion	bj-nfcf	⊢ ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		bj-nfcf.nf	⊢ Ⅎ 𝑦 𝐴
2		df-nfc	⊢ ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑧 Ⅎ 𝑥 𝑧 ∈ 𝐴 )
3	1	nfcri	⊢ Ⅎ 𝑦 𝑧 ∈ 𝐴
4	3	nfnf	⊢ Ⅎ 𝑦 Ⅎ 𝑥 𝑧 ∈ 𝐴
5	4	sb8v	⊢ ( ∀ 𝑧 Ⅎ 𝑥 𝑧 ∈ 𝐴 ↔ ∀ 𝑦 [ 𝑦 / 𝑧 ] Ⅎ 𝑥 𝑧 ∈ 𝐴 )
6		bj-sbnf	⊢ ( [ 𝑦 / 𝑧 ] Ⅎ 𝑥 𝑧 ∈ 𝐴 ↔ Ⅎ 𝑥 [ 𝑦 / 𝑧 ] 𝑧 ∈ 𝐴 )
7		clelsb1	⊢ ( [ 𝑦 / 𝑧 ] 𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 )
8	7	nfbii	⊢ ( Ⅎ 𝑥 [ 𝑦 / 𝑧 ] 𝑧 ∈ 𝐴 ↔ Ⅎ 𝑥 𝑦 ∈ 𝐴 )
9	6 8	bitri	⊢ ( [ 𝑦 / 𝑧 ] Ⅎ 𝑥 𝑧 ∈ 𝐴 ↔ Ⅎ 𝑥 𝑦 ∈ 𝐴 )
10	9	albii	⊢ ( ∀ 𝑦 [ 𝑦 / 𝑧 ] Ⅎ 𝑥 𝑧 ∈ 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴 )
11	5 10	bitri	⊢ ( ∀ 𝑧 Ⅎ 𝑥 𝑧 ∈ 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴 )
12	2 11	bitri	⊢ ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴 )