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	$$⊢Ⅎy\phi$$
	nfcd.2	$$⊢\phi \to Ⅎxy\in A$$
Assertion	nfcd	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$

Proof

Step	Hyp	Ref	Expression
1		nfcd.1	$$⊢Ⅎy\phi$$
2		nfcd.2	$$⊢\phi \to Ⅎxy\in A$$
3	1 2	alrimi	$$⊢\phi \to \forall yℲxy\in A$$
4		df-nfc	$$⊢\underset{\_}{Ⅎ}xA\leftrightarrow \forall yℲxy\in A$$
5	3 4	sylibr	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$