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

Metamath Proof Explorer

Theorem nfcr

Description: Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016) Drop ax-12 but use ax-8 , df-clel , and avoid a DV condition on y , A . (Revised by SN, 3-Jun-2024)

Ref Expression
Assertion nfcr ⊢ Ⅎ _ x A → Ⅎ x y ∈ A

Proof

Step Hyp Ref Expression
1 df-nfc ⊢ Ⅎ _ x A ↔ ∀ z Ⅎ x z ∈ A
2 eleq1w ⊢ z = y → z ∈ A ↔ y ∈ A
3 2 nfbidv ⊢ z = y → Ⅎ x z ∈ A ↔ Ⅎ x y ∈ A
4 3 spvv ⊢ ∀ z Ⅎ x z ∈ A → Ⅎ x y ∈ A
5 1 4 sylbi ⊢ Ⅎ _ x A → Ⅎ x y ∈ A