Proof of Theorem zfcndpow
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dtru 5440 | . . . . 5
⊢  ¬
∀𝑦 𝑦 = 𝑧 | 
| 2 |  | exnal 1826 | . . . . 5
⊢
(∃𝑦 ¬
𝑦 = 𝑧 ↔ ¬ ∀𝑦 𝑦 = 𝑧) | 
| 3 | 1, 2 | mpbir 231 | . . . 4
⊢
∃𝑦 ¬ 𝑦 = 𝑧 | 
| 4 |  | nfe1 2149 | . . . . 5
⊢
Ⅎ𝑦∃𝑦∀𝑧(∀𝑦(∃𝑥 𝑦 ∈ 𝑧 → ∀𝑧 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦) | 
| 5 |  | axpownd 10642 | . . . . 5
⊢ (¬
𝑦 = 𝑧 → ∃𝑦∀𝑧(∀𝑦(∃𝑥 𝑦 ∈ 𝑧 → ∀𝑧 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦)) | 
| 6 | 4, 5 | exlimi 2216 | . . . 4
⊢
(∃𝑦 ¬
𝑦 = 𝑧 → ∃𝑦∀𝑧(∀𝑦(∃𝑥 𝑦 ∈ 𝑧 → ∀𝑧 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦)) | 
| 7 | 3, 6 | ax-mp 5 | . . 3
⊢
∃𝑦∀𝑧(∀𝑦(∃𝑥 𝑦 ∈ 𝑧 → ∀𝑧 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦) | 
| 8 |  | 19.9v 1982 | . . . . . . . 8
⊢
(∃𝑥 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧) | 
| 9 |  | 19.3v 1980 | . . . . . . . 8
⊢
(∀𝑧 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥) | 
| 10 | 8, 9 | imbi12i 350 | . . . . . . 7
⊢
((∃𝑥 𝑦 ∈ 𝑧 → ∀𝑧 𝑦 ∈ 𝑥) ↔ (𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥)) | 
| 11 | 10 | albii 1818 | . . . . . 6
⊢
(∀𝑦(∃𝑥 𝑦 ∈ 𝑧 → ∀𝑧 𝑦 ∈ 𝑥) ↔ ∀𝑦(𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥)) | 
| 12 | 11 | imbi1i 349 | . . . . 5
⊢
((∀𝑦(∃𝑥 𝑦 ∈ 𝑧 → ∀𝑧 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ (∀𝑦(𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦)) | 
| 13 | 12 | albii 1818 | . . . 4
⊢
(∀𝑧(∀𝑦(∃𝑥 𝑦 ∈ 𝑧 → ∀𝑧 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∀𝑧(∀𝑦(𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦)) | 
| 14 | 13 | exbii 1847 | . . 3
⊢
(∃𝑦∀𝑧(∀𝑦(∃𝑥 𝑦 ∈ 𝑧 → ∀𝑧 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∃𝑦∀𝑧(∀𝑦(𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦)) | 
| 15 | 7, 14 | mpbi 230 | . 2
⊢
∃𝑦∀𝑧(∀𝑦(𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦) | 
| 16 |  | elequ1 2114 | . . . . . . 7
⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧)) | 
| 17 |  | elequ1 2114 | . . . . . . 7
⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) | 
| 18 | 16, 17 | imbi12d 344 | . . . . . 6
⊢ (𝑤 = 𝑦 → ((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) ↔ (𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥))) | 
| 19 | 18 | cbvalvw 2034 | . . . . 5
⊢
(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) ↔ ∀𝑦(𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥)) | 
| 20 | 19 | imbi1i 349 | . . . 4
⊢
((∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ (∀𝑦(𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦)) | 
| 21 | 20 | albii 1818 | . . 3
⊢
(∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∀𝑧(∀𝑦(𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦)) | 
| 22 | 21 | exbii 1847 | . 2
⊢
(∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∃𝑦∀𝑧(∀𝑦(𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦)) | 
| 23 | 15, 22 | mpbir 231 | 1
⊢
∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) |