Metamath Proof Explorer

Theorem nfcri

Description: Consequence of the not-free predicate. (Note that unlike nfcr , this does not require y and A to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016) Avoid ax-10 , ax-11 . (Revised by Gino Giotto, 23-May-2024) Avoid ax-12 . (Revised by SN, 26-May-2024)

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

Proof

Step Hyp Ref Expression
1 nfcri.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 eleq1w ⊢ z = w → z ∈ A ↔ w ∈ A
9 8 exbidv ⊢ z = w → ∃ x z ∈ A ↔ ∃ x w ∈ A
10 8 albidv ⊢ z = w → ∀ x z ∈ A ↔ ∀ x w ∈ A
11 9 10 imbi12d ⊢ z = w → ∃ x z ∈ A → ∀ x z ∈ A ↔ ∃ x w ∈ A → ∀ x w ∈ A
12 11 spw ⊢ ∀ z ∃ x z ∈ A → ∀ x z ∈ A → ∃ x z ∈ A → ∀ x z ∈ A
13 7 12 sylbi ⊢ ∀ z Ⅎ x z ∈ A → ∃ x z ∈ A → ∀ x z ∈ A
14 1 5 13 mp2b ⊢ ∃ x z ∈ A → ∀ x z ∈ A
15 14 nfi ⊢ Ⅎ x z ∈ A
16 3 15 chvarvv ⊢ Ⅎ x y ∈ A