Metamath Proof Explorer

Theorem nfcriOLDOLD

Description: Obsolete version of nfcri as of 26-May-2024. (Contributed by Mario Carneiro, 11-Aug-2016) Avoid ax-10 , ax-11 . (Revised by Gino Giotto, 23-May-2024) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis nfcrii.1 ⊢ Ⅎ _ x A
Assertion nfcriOLDOLD ⊢ Ⅎ x y ∈ A

Proof

Step Hyp Ref Expression
1 nfcrii.1 ⊢ Ⅎ _ x A
2 eleq1w ⊢ z = y → z ∈ A ↔ y ∈ A
3 2 nfbidv ⊢ z = y → Ⅎ x z ∈ A ↔ Ⅎ x y ∈ A
4 df-nfc ⊢ Ⅎ _ x A ↔ ∀ z Ⅎ x z ∈ A
5 4 biimpi ⊢ Ⅎ _ x A → ∀ z Ⅎ x z ∈ A
6 df-nf ⊢ Ⅎ x z ∈ A ↔ ∃ x z ∈ A → ∀ x z ∈ A
7 6 albii ⊢ ∀ z Ⅎ x z ∈ A ↔ ∀ z ∃ x z ∈ A → ∀ x z ∈ A
8 sp ⊢ ∀ z ∃ x z ∈ A → ∀ x z ∈ A → ∃ x z ∈ A → ∀ x z ∈ A
9 7 8 sylbi ⊢ ∀ z Ⅎ x z ∈ A → ∃ x z ∈ A → ∀ x z ∈ A
10 1 5 9 mp2b ⊢ ∃ x z ∈ A → ∀ x z ∈ A
11 10 nfi ⊢ Ⅎ x z ∈ A
12 3 11 chvarvv ⊢ Ⅎ x y ∈ A