Theorem nfnfc1

Description: The setvar x is bound in F/_ x A . (Contributed by Mario Carneiro, 11-Aug-2016)

	Ref	Expression
Assertion	nfnfc1	⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝐴

Proof

Step	Hyp	Ref	Expression
1		df-nfc	⊢ ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴 )
2		nfnf1	⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝑦 ∈ 𝐴
3	2	nfal	⊢ Ⅎ 𝑥 ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴
4	1 3	nfxfr	⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝐴