Theorem nfcd

Description: Deduce that a class A does not have x free in it. (Contributed by Mario Carneiro, 11-Aug-2016)

	Ref	Expression
Hypotheses	nfcd.1	⊢ Ⅎ 𝑦 𝜑
	nfcd.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 ∈ 𝐴 )
Assertion	nfcd	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nfcd.1	⊢ Ⅎ 𝑦 𝜑
2		nfcd.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 ∈ 𝐴 )
3	1 2	alrimi	⊢ ( 𝜑 → ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴 )
4		df-nfc	⊢ ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴 )
5	3 4	sylibr	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )