Proof of Theorem 2sb5ndVD
Step | Hyp | Ref
| Expression |
1 | | ax6e2ndeq 42147 |
. 2
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) |
2 | | anabs5 660 |
. . . 4
⊢
((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) |
3 | | 2pm13.193 42140 |
. . . . . . . . 9
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)) |
4 | 3 | exbii 1854 |
. . . . . . . 8
⊢
(∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)) |
5 | | hbs1 2270 |
. . . . . . . . . . . . 13
⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) |
6 | | idn1 42162 |
. . . . . . . . . . . . . 14
⊢ ( ∀𝑥 𝑥 = 𝑦 ▶ ∀𝑥 𝑥 = 𝑦 ) |
7 | | axc11 2432 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 𝑥 = 𝑦 → (∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) |
8 | 6, 7 | e1a 42215 |
. . . . . . . . . . . . 13
⊢ ( ∀𝑥 𝑥 = 𝑦 ▶ (∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ) |
9 | | imim1 83 |
. . . . . . . . . . . . 13
⊢ (([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → ((∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))) |
10 | 5, 8, 9 | e01 42279 |
. . . . . . . . . . . 12
⊢ ( ∀𝑥 𝑥 = 𝑦 ▶ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ) |
11 | 10 | in1 42159 |
. . . . . . . . . . 11
⊢
(∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) |
12 | | hbs1 2270 |
. . . . . . . . . . . . . . 15
⊢ ([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑) |
13 | 12 | sbt 2073 |
. . . . . . . . . . . . . 14
⊢ [𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑) |
14 | | sbi1 2078 |
. . . . . . . . . . . . . 14
⊢ ([𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑)) |
15 | 13, 14 | e0a 42360 |
. . . . . . . . . . . . 13
⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑) |
16 | | idn1 42162 |
. . . . . . . . . . . . . . 15
⊢ ( ¬ ∀𝑥 𝑥 = 𝑦 ▶ ¬
∀𝑥 𝑥 = 𝑦 ) |
17 | | axc11n 2428 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑥 = 𝑦) |
18 | 17 | con3i 154 |
. . . . . . . . . . . . . . 15
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑦 𝑦 = 𝑥) |
19 | 16, 18 | e1a 42215 |
. . . . . . . . . . . . . 14
⊢ ( ¬ ∀𝑥 𝑥 = 𝑦 ▶ ¬
∀𝑦 𝑦 = 𝑥 ) |
20 | | sbal2 2536 |
. . . . . . . . . . . . . 14
⊢ (¬
∀𝑦 𝑦 = 𝑥 → ([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) |
21 | 19, 20 | e1a 42215 |
. . . . . . . . . . . . 13
⊢ ( ¬ ∀𝑥 𝑥 = 𝑦 ▶ ([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ) |
22 | | imbi2 349 |
. . . . . . . . . . . . . 14
⊢ (([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → (([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))) |
23 | 22 | biimpcd 248 |
. . . . . . . . . . . . 13
⊢ (([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑) → (([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))) |
24 | 15, 21, 23 | e01 42279 |
. . . . . . . . . . . 12
⊢ ( ¬ ∀𝑥 𝑥 = 𝑦 ▶ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ) |
25 | 24 | in1 42159 |
. . . . . . . . . . 11
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) |
26 | 11, 25 | pm2.61i 182 |
. . . . . . . . . 10
⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) |
27 | 26 | nf5i 2146 |
. . . . . . . . 9
⊢
Ⅎ𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑 |
28 | 27 | 19.41 2232 |
. . . . . . . 8
⊢
(∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) |
29 | 4, 28 | bitr3i 276 |
. . . . . . 7
⊢
(∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ↔ (∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) |
30 | 29 | exbii 1854 |
. . . . . 6
⊢
(∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ↔ ∃𝑥(∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) |
31 | 5 | nf5i 2146 |
. . . . . . 7
⊢
Ⅎ𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑 |
32 | 31 | 19.41 2232 |
. . . . . 6
⊢
(∃𝑥(∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) |
33 | 30, 32 | bitr2i 275 |
. . . . 5
⊢
((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)) |
34 | 33 | anbi2i 623 |
. . . 4
⊢
((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))) |
35 | 2, 34 | bitr3i 276 |
. . 3
⊢
((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))) |
36 | | pm5.32 574 |
. . 3
⊢
((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))) ↔ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))) |
37 | 35, 36 | mpbir 230 |
. 2
⊢
(∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))) |
38 | 1, 37 | sylbi 216 |
1
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))) |