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

Metamath Proof Explorer

Theorem nfcd

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

Ref Expression
Hypotheses nfcd.1 ⊢ Ⅎ y φ
nfcd.2 ⊢ φ → Ⅎ x y ∈ A
Assertion nfcd ⊢ φ → Ⅎ _ x A

Proof

Step Hyp Ref Expression
1 nfcd.1 ⊢ Ⅎ y φ
2 nfcd.2 ⊢ φ → Ⅎ x y ∈ A
3 1 2 alrimi ⊢ φ → ∀ y Ⅎ x y ∈ A
4 df-nfc ⊢ Ⅎ _ x A ↔ ∀ y Ⅎ x y ∈ A
5 3 4 sylibr ⊢ φ → Ⅎ _ x A