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

Metamath Proof Explorer

Theorem nfcrd

Description: Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016)

Ref Expression
Hypothesis nfcrd.1 ⊢ φ → Ⅎ _ x A
Assertion nfcrd ⊢ φ → Ⅎ x y ∈ A

Proof

Step Hyp Ref Expression
1 nfcrd.1 ⊢ φ → Ⅎ _ x A
2 nfcr ⊢ Ⅎ _ x A → Ⅎ x y ∈ A
3 1 2 syl ⊢ φ → Ⅎ x y ∈ A