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

Metamath Proof Explorer

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 ⊢ Ⅎ x y ∈ A
Assertion nfci ⊢ Ⅎ _ x A

Proof

Step Hyp Ref Expression
1 nfci.1 ⊢ Ⅎ x y ∈ A
2 df-nfc ⊢ Ⅎ _ x A ↔ ∀ y Ⅎ x y ∈ A
3 2 1 mpgbir ⊢ Ⅎ _ x A