This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfnfc1

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

Ref Expression
Assertion nfnfc1 ⊢ Ⅎ x Ⅎ _ x A

Proof

Step Hyp Ref Expression
1 df-nfc ⊢ Ⅎ _ x A ↔ ∀ y Ⅎ x y ∈ A
2 nfnf1 ⊢ Ⅎ x Ⅎ x y ∈ A
3 2 nfal ⊢ Ⅎ x ∀ y Ⅎ x y ∈ A
4 1 3 nfxfr ⊢ Ⅎ x Ⅎ _ x A