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	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
Assertion	nfci	⊢ Ⅎ 𝑥 𝐴

Proof

Step	Hyp	Ref	Expression
1		nfci.1	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
2		df-nfc	⊢ ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴 )
3	2 1	mpgbir	⊢ Ⅎ 𝑥 𝐴