Proof of Theorem 2sb6rf
Step | Hyp | Ref
| Expression |
1 | | sbequ12r 2098 |
. . . . 5
⊢ (𝑧 = 𝑥 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑤 / 𝑦]𝜑)) |
2 | | sbequ12r 2098 |
. . . . 5
⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑦]𝜑 ↔ 𝜑)) |
3 | 1, 2 | sylan9bb 732 |
. . . 4
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ 𝜑)) |
4 | 3 | pm5.74i 259 |
. . 3
⊢ (((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) ↔ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → 𝜑)) |
5 | 4 | 2albii 1738 |
. 2
⊢
(∀𝑧∀𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) ↔ ∀𝑧∀𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → 𝜑)) |
6 | | 2sb5rf.2 |
. . . . 5
⊢
Ⅎ𝑤𝜑 |
7 | 6 | 19.23 2067 |
. . . 4
⊢
(∀𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → 𝜑) ↔ (∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → 𝜑)) |
8 | 7 | albii 1737 |
. . 3
⊢
(∀𝑧∀𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → 𝜑) ↔ ∀𝑧(∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → 𝜑)) |
9 | | 2sb5rf.1 |
. . . 4
⊢
Ⅎ𝑧𝜑 |
10 | 9 | 19.23 2067 |
. . 3
⊢
(∀𝑧(∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → 𝜑) ↔ (∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → 𝜑)) |
11 | 8, 10 | bitri 263 |
. 2
⊢
(∀𝑧∀𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → 𝜑) ↔ (∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → 𝜑)) |
12 | | 2ax6e 2438 |
. . 3
⊢
∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦) |
13 | | pm5.5 350 |
. . 3
⊢
(∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → ((∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → 𝜑) ↔ 𝜑)) |
14 | 12, 13 | ax-mp 5 |
. 2
⊢
((∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → 𝜑) ↔ 𝜑) |
15 | 5, 11, 14 | 3bitrri 286 |
1
⊢ (𝜑 ↔ ∀𝑧∀𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)) |