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 𝑥 𝐴
Assertion nfcri 𝑥 𝑦𝐴

Proof

Step Hyp Ref Expression
1 nfcri.1 𝑥 𝐴
2 eleq1w ( 𝑧 = 𝑦 → ( 𝑧𝐴𝑦𝐴 ) )
3 2 nfbidv ( 𝑧 = 𝑦 → ( Ⅎ 𝑥 𝑧𝐴 ↔ Ⅎ 𝑥 𝑦𝐴 ) )
4 df-nfc ( 𝑥 𝐴 ↔ ∀ 𝑧𝑥 𝑧𝐴 )
5 4 biimpi ( 𝑥 𝐴 → ∀ 𝑧𝑥 𝑧𝐴 )
6 df-nf ( Ⅎ 𝑥 𝑧𝐴 ↔ ( ∃ 𝑥 𝑧𝐴 → ∀ 𝑥 𝑧𝐴 ) )
7 6 albii ( ∀ 𝑧𝑥 𝑧𝐴 ↔ ∀ 𝑧 ( ∃ 𝑥 𝑧𝐴 → ∀ 𝑥 𝑧𝐴 ) )
8 eleq1w ( 𝑧 = 𝑤 → ( 𝑧𝐴𝑤𝐴 ) )
9 8 exbidv ( 𝑧 = 𝑤 → ( ∃ 𝑥 𝑧𝐴 ↔ ∃ 𝑥 𝑤𝐴 ) )
10 8 albidv ( 𝑧 = 𝑤 → ( ∀ 𝑥 𝑧𝐴 ↔ ∀ 𝑥 𝑤𝐴 ) )
11 9 10 imbi12d ( 𝑧 = 𝑤 → ( ( ∃ 𝑥 𝑧𝐴 → ∀ 𝑥 𝑧𝐴 ) ↔ ( ∃ 𝑥 𝑤𝐴 → ∀ 𝑥 𝑤𝐴 ) ) )
12 11 spw ( ∀ 𝑧 ( ∃ 𝑥 𝑧𝐴 → ∀ 𝑥 𝑧𝐴 ) → ( ∃ 𝑥 𝑧𝐴 → ∀ 𝑥 𝑧𝐴 ) )
13 7 12 sylbi ( ∀ 𝑧𝑥 𝑧𝐴 → ( ∃ 𝑥 𝑧𝐴 → ∀ 𝑥 𝑧𝐴 ) )
14 1 5 13 mp2b ( ∃ 𝑥 𝑧𝐴 → ∀ 𝑥 𝑧𝐴 )
15 14 nfi 𝑥 𝑧𝐴
16 3 15 chvarvv 𝑥 𝑦𝐴