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

Metamath Proof Explorer

Theorem nfcrALT

Description: Alternate version of nfcr . Avoids ax-8 but uses ax-12 . (Contributed by Mario Carneiro, 11-Aug-2016) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 df-nfc ⊢ Ⅎ _ x A ↔ ∀ y Ⅎ x y ∈ A
2 sp ⊢ ∀ y Ⅎ x y ∈ A → Ⅎ x y ∈ A
3 1 2 sylbi ⊢ Ⅎ _ x A → Ⅎ x y ∈ A