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	⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 𝑦 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-nfc	⊢ ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑧 Ⅎ 𝑥 𝑧 ∈ 𝐴 )
2		eleq1w	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
3	2	nfbidv	⊢ ( 𝑧 = 𝑦 → ( Ⅎ 𝑥 𝑧 ∈ 𝐴 ↔ Ⅎ 𝑥 𝑦 ∈ 𝐴 ) )
4	3	spvv	⊢ ( ∀ 𝑧 Ⅎ 𝑥 𝑧 ∈ 𝐴 → Ⅎ 𝑥 𝑦 ∈ 𝐴 )
5	1 4	sylbi	⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 𝑦 ∈ 𝐴 )