| Step | Hyp | Ref
| Expression |
| 1 | | vex 3484 |
. . . . . . 7
⊢ 𝑢 ∈ V |
| 2 | | ax6e 2388 |
. . . . . . 7
⊢
∃𝑦 𝑦 = 𝑣 |
| 3 | 1, 2 | pm3.2i 470 |
. . . . . 6
⊢ (𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣) |
| 4 | | 19.42v 1953 |
. . . . . . 7
⊢
(∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ (𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣)) |
| 5 | 4 | biimpri 228 |
. . . . . 6
⊢ ((𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣) → ∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣)) |
| 6 | 3, 5 | ax-mp 5 |
. . . . 5
⊢
∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣) |
| 7 | | isset 3494 |
. . . . . . 7
⊢ (𝑢 ∈ V ↔ ∃𝑥 𝑥 = 𝑢) |
| 8 | 7 | anbi1i 624 |
. . . . . 6
⊢ ((𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ (∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) |
| 9 | 8 | exbii 1848 |
. . . . 5
⊢
(∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ ∃𝑦(∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) |
| 10 | 6, 9 | mpbi 230 |
. . . 4
⊢
∃𝑦(∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) |
| 11 | | id 22 |
. . . . . 6
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦) |
| 12 | | hbnae 2437 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦) |
| 13 | | hbn1 2142 |
. . . . . . . . . . . 12
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑦) |
| 14 | | ax-5 1910 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑣 → ∀𝑥 𝑧 = 𝑣) |
| 15 | | ax-5 1910 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑣 → ∀𝑧 𝑦 = 𝑣) |
| 16 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑦 → 𝑧 = 𝑦) |
| 17 | | equequ1 2024 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑦 → (𝑧 = 𝑣 ↔ 𝑦 = 𝑣)) |
| 18 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 = 𝑦 → 𝑧 = 𝑦) → (𝑧 = 𝑦 → (𝑧 = 𝑣 ↔ 𝑦 = 𝑣))) |
| 19 | 16, 18 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑦 → (𝑧 = 𝑣 ↔ 𝑦 = 𝑣)) |
| 20 | 14, 15, 19 | dvelimh 2455 |
. . . . . . . . . . . . . . 15
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣)) |
| 21 | 11, 20 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣)) |
| 22 | 21 | idiALT 44498 |
. . . . . . . . . . . . 13
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣)) |
| 23 | 22 | alimi 1811 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ¬
∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣)) |
| 24 | 13, 23 | syl 17 |
. . . . . . . . . . 11
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣)) |
| 25 | 11, 24 | syl 17 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣)) |
| 26 | | 19.41rg 44570 |
. . . . . . . . . 10
⊢
(∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣) → ((∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) |
| 27 | 25, 26 | syl 17 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ((∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) |
| 28 | 27 | idiALT 44498 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ((∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) |
| 29 | 28 | alimi 1811 |
. . . . . . 7
⊢
(∀𝑦 ¬
∀𝑥 𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) |
| 30 | 12, 29 | syl 17 |
. . . . . 6
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) |
| 31 | 11, 30 | syl 17 |
. . . . 5
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) |
| 32 | | exim 1834 |
. . . . 5
⊢
(∀𝑦((∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → (∃𝑦(∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) |
| 33 | 31, 32 | syl 17 |
. . . 4
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑦(∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) |
| 34 | | pm3.35 803 |
. . . 4
⊢
((∃𝑦(∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (∃𝑦(∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) → ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) |
| 35 | 10, 33, 34 | sylancr 587 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) |
| 36 | | excomim 2163 |
. . 3
⊢
(∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) |
| 37 | 35, 36 | syl 17 |
. 2
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) |
| 38 | 37 | idiALT 44498 |
1
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) |