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

Metamath Proof Explorer

Theorem nfcjust

Description: Justification theorem for df-nfc . (Contributed by Mario Carneiro, 13-Oct-2016)

Ref Expression
Assertion nfcjust ⊢ ∀ y Ⅎ x y ∈ A ↔ ∀ z Ⅎ x z ∈ A

Proof

Step Hyp Ref Expression
1 eleq1w ⊢ y = z → y ∈ A ↔ z ∈ A
2 1 nfbidv ⊢ y = z → Ⅎ x y ∈ A ↔ Ⅎ x z ∈ A
3 2 cbvalvw ⊢ ∀ y Ⅎ x y ∈ A ↔ ∀ z Ⅎ x z ∈ A