![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfcriOLD | Structured version Visualization version GIF version |
Description: Obsolete version of nfcri 2904 as of 3-Jun-2024. (Contributed by Mario Carneiro, 11-Aug-2016.) Avoid ax-10 2143, ax-11 2159. (Revised by Gino Giotto, 23-May-2024.) Avoid ax-12 2176. (Revised by SN, 26-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
nfcrii.1 | ⊢ Ⅎ𝑥𝐴 |
Ref | Expression |
---|---|
nfcriOLD | ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1w 2833 | . . 3 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
2 | 1 | nfbidv 1924 | . 2 ⊢ (𝑧 = 𝑦 → (Ⅎ𝑥 𝑧 ∈ 𝐴 ↔ Ⅎ𝑥 𝑦 ∈ 𝐴)) |
3 | nfcrii.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
4 | df-nfc 2899 | . . . . 5 ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑧Ⅎ𝑥 𝑧 ∈ 𝐴) | |
5 | 4 | biimpi 219 | . . . 4 ⊢ (Ⅎ𝑥𝐴 → ∀𝑧Ⅎ𝑥 𝑧 ∈ 𝐴) |
6 | df-nf 1787 | . . . . . 6 ⊢ (Ⅎ𝑥 𝑧 ∈ 𝐴 ↔ (∃𝑥 𝑧 ∈ 𝐴 → ∀𝑥 𝑧 ∈ 𝐴)) | |
7 | 6 | albii 1822 | . . . . 5 ⊢ (∀𝑧Ⅎ𝑥 𝑧 ∈ 𝐴 ↔ ∀𝑧(∃𝑥 𝑧 ∈ 𝐴 → ∀𝑥 𝑧 ∈ 𝐴)) |
8 | eleq1w 2833 | . . . . . . . 8 ⊢ (𝑧 = 𝑤 → (𝑧 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) | |
9 | 8 | exbidv 1923 | . . . . . . 7 ⊢ (𝑧 = 𝑤 → (∃𝑥 𝑧 ∈ 𝐴 ↔ ∃𝑥 𝑤 ∈ 𝐴)) |
10 | 8 | albidv 1922 | . . . . . . 7 ⊢ (𝑧 = 𝑤 → (∀𝑥 𝑧 ∈ 𝐴 ↔ ∀𝑥 𝑤 ∈ 𝐴)) |
11 | 9, 10 | imbi12d 349 | . . . . . 6 ⊢ (𝑧 = 𝑤 → ((∃𝑥 𝑧 ∈ 𝐴 → ∀𝑥 𝑧 ∈ 𝐴) ↔ (∃𝑥 𝑤 ∈ 𝐴 → ∀𝑥 𝑤 ∈ 𝐴))) |
12 | 11 | spw 2042 | . . . . 5 ⊢ (∀𝑧(∃𝑥 𝑧 ∈ 𝐴 → ∀𝑥 𝑧 ∈ 𝐴) → (∃𝑥 𝑧 ∈ 𝐴 → ∀𝑥 𝑧 ∈ 𝐴)) |
13 | 7, 12 | sylbi 220 | . . . 4 ⊢ (∀𝑧Ⅎ𝑥 𝑧 ∈ 𝐴 → (∃𝑥 𝑧 ∈ 𝐴 → ∀𝑥 𝑧 ∈ 𝐴)) |
14 | 3, 5, 13 | mp2b 10 | . . 3 ⊢ (∃𝑥 𝑧 ∈ 𝐴 → ∀𝑥 𝑧 ∈ 𝐴) |
15 | 14 | nfi 1791 | . 2 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐴 |
16 | 2, 15 | chvarvv 2006 | 1 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1537 ∃wex 1782 Ⅎwnf 1786 ∈ wcel 2112 Ⅎwnfc 2897 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 |
This theorem depends on definitions: df-bi 210 df-an 401 df-ex 1783 df-nf 1787 df-clel 2831 df-nfc 2899 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |