| Step | Hyp | Ref
| Expression |
| 1 | | en2lp 9646 |
. . . . . . . 8
⊢ ¬
(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦) |
| 2 | | elequ2 2123 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧)) |
| 3 | 2 | anbi2d 630 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦) ↔ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧))) |
| 4 | 1, 3 | mtbii 326 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → ¬ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
| 5 | 4 | sps 2185 |
. . . . . 6
⊢
(∀𝑦 𝑦 = 𝑧 → ¬ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
| 6 | 5 | nexdv 1936 |
. . . . 5
⊢
(∀𝑦 𝑦 = 𝑧 → ¬ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
| 7 | 6 | pm2.21d 121 |
. . . 4
⊢
(∀𝑦 𝑦 = 𝑧 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
| 8 | 7 | axc4i 2322 |
. . 3
⊢
(∀𝑦 𝑦 = 𝑧 → ∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
| 9 | 8 | 19.8ad 2182 |
. 2
⊢
(∀𝑦 𝑦 = 𝑧 → ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
| 10 | | zfun 7756 |
. . 3
⊢
∃𝑥∀𝑤(∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥) |
| 11 | | nfnae 2439 |
. . . . 5
⊢
Ⅎ𝑦 ¬
∀𝑦 𝑦 = 𝑧 |
| 12 | | nfnae 2439 |
. . . . . . 7
⊢
Ⅎ𝑥 ¬
∀𝑦 𝑦 = 𝑧 |
| 13 | | nfvd 1915 |
. . . . . . . 8
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦 𝑤 ∈ 𝑥) |
| 14 | | nfcvf 2932 |
. . . . . . . . 9
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦𝑧) |
| 15 | 14 | nfcrd 2899 |
. . . . . . . 8
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦 𝑥 ∈ 𝑧) |
| 16 | 13, 15 | nfand 1897 |
. . . . . . 7
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
| 17 | 12, 16 | nfexd 2329 |
. . . . . 6
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
| 18 | 17, 13 | nfimd 1894 |
. . . . 5
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦(∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥)) |
| 19 | | elequ1 2115 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) |
| 20 | 19 | anbi1d 631 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → ((𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) ↔ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧))) |
| 21 | 20 | exbidv 1921 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) ↔ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧))) |
| 22 | 21, 19 | imbi12d 344 |
. . . . . 6
⊢ (𝑤 = 𝑦 → ((∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
| 23 | 22 | a1i 11 |
. . . . 5
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (𝑤 = 𝑦 → ((∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)))) |
| 24 | 11, 18, 23 | cbvald 2412 |
. . . 4
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∀𝑤(∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥) ↔ ∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
| 25 | 24 | exbidv 1921 |
. . 3
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∃𝑥∀𝑤(∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥) ↔ ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
| 26 | 10, 25 | mpbii 233 |
. 2
⊢ (¬
∀𝑦 𝑦 = 𝑧 → ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
| 27 | 9, 26 | pm2.61i 182 |
1
⊢
∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) |