Proof of Theorem sb7fALT
Step | Hyp | Ref
| Expression |
1 | | biid 263 |
. . 3
⊢ (((𝑧 = 𝑦 → ((𝑥 = 𝑧 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) ∧ ∃𝑧(𝑧 = 𝑦 ∧ ((𝑥 = 𝑧 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)))) ↔ ((𝑧 = 𝑦 → ((𝑥 = 𝑧 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) ∧ ∃𝑧(𝑧 = 𝑦 ∧ ((𝑥 = 𝑧 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))))) |
2 | | biid 263 |
. . 3
⊢ (((𝑧 = 𝑦 → ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)) ∧ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) ↔ ((𝑧 = 𝑦 → ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)) ∧ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)))) |
3 | | biid 263 |
. . . 4
⊢ (((𝑥 = 𝑧 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)) ↔ ((𝑥 = 𝑧 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) |
4 | | sb7fALT.1 |
. . . 4
⊢
Ⅎ𝑧𝜑 |
5 | 3, 4 | sb5fALT 2602 |
. . 3
⊢ (((𝑥 = 𝑧 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)) ↔ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)) |
6 | 1, 2, 5 | sbbiiALT 2577 |
. 2
⊢ (((𝑧 = 𝑦 → ((𝑥 = 𝑧 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) ∧ ∃𝑧(𝑧 = 𝑦 ∧ ((𝑥 = 𝑧 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)))) ↔ ((𝑧 = 𝑦 → ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)) ∧ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)))) |
7 | | dfsb1.p9 |
. . 3
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) |
8 | 7, 1, 4 | sbco2ALT 2614 |
. 2
⊢ (((𝑧 = 𝑦 → ((𝑥 = 𝑧 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) ∧ ∃𝑧(𝑧 = 𝑦 ∧ ((𝑥 = 𝑧 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)))) ↔ 𝜃) |
9 | 2 | sb5ALT2 2585 |
. 2
⊢ (((𝑧 = 𝑦 → ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)) ∧ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) |
10 | 6, 8, 9 | 3bitr3i 303 |
1
⊢ (𝜃 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) |