Theorem nfci

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

	Ref	Expression
Hypothesis	nfci.1	|- F/ x y e. A
Assertion	nfci	|- F/_ x A

Proof

Step	Hyp	Ref	Expression
1		nfci.1	|- F/ x y e. A
2		df-nfc	|- ( F/_ x A <-> A. y F/ x y e. A )
3	2 1	mpgbir	|- F/_ x A