Proof of Theorem sbbiALT
Step | Hyp | Ref
| Expression |
1 | | dfsb1.bi |
. . 3
⊢ (𝜂 ↔ ((𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜑 ↔ 𝜓)))) |
2 | | biid 263 |
. . 3
⊢ (((𝑥 = 𝑦 → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ ∃𝑥(𝑥 = 𝑦 ∧ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))) ↔ ((𝑥 = 𝑦 → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ ∃𝑥(𝑥 = 𝑦 ∧ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))))) |
3 | | dfbi2 477 |
. . 3
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) |
4 | 1, 2, 3 | sbbiiALT 2577 |
. 2
⊢ (𝜂 ↔ ((𝑥 = 𝑦 → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ ∃𝑥(𝑥 = 𝑦 ∧ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))))) |
5 | | dfsb1.p6 |
. . . . 5
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) |
6 | | dfsb1.s4 |
. . . . 5
⊢ (𝜏 ↔ ((𝑥 = 𝑦 → 𝜓) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))) |
7 | | biid 263 |
. . . . 5
⊢ (((𝑥 = 𝑦 → (𝜑 → 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜑 → 𝜓))) ↔ ((𝑥 = 𝑦 → (𝜑 → 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜑 → 𝜓)))) |
8 | 5, 6, 7 | sbimALT 2607 |
. . . 4
⊢ (((𝑥 = 𝑦 → (𝜑 → 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜑 → 𝜓))) ↔ (𝜃 → 𝜏)) |
9 | | biid 263 |
. . . . 5
⊢ (((𝑥 = 𝑦 → (𝜓 → 𝜑)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜓 → 𝜑))) ↔ ((𝑥 = 𝑦 → (𝜓 → 𝜑)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜓 → 𝜑)))) |
10 | 6, 5, 9 | sbimALT 2607 |
. . . 4
⊢ (((𝑥 = 𝑦 → (𝜓 → 𝜑)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜓 → 𝜑))) ↔ (𝜏 → 𝜃)) |
11 | 8, 10 | anbi12i 628 |
. . 3
⊢ ((((𝑥 = 𝑦 → (𝜑 → 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜑 → 𝜓))) ∧ ((𝑥 = 𝑦 → (𝜓 → 𝜑)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜓 → 𝜑)))) ↔ ((𝜃 → 𝜏) ∧ (𝜏 → 𝜃))) |
12 | 7, 9, 2 | sbanALT 2609 |
. . 3
⊢ (((𝑥 = 𝑦 → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ ∃𝑥(𝑥 = 𝑦 ∧ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))) ↔ (((𝑥 = 𝑦 → (𝜑 → 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜑 → 𝜓))) ∧ ((𝑥 = 𝑦 → (𝜓 → 𝜑)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜓 → 𝜑))))) |
13 | | dfbi2 477 |
. . 3
⊢ ((𝜃 ↔ 𝜏) ↔ ((𝜃 → 𝜏) ∧ (𝜏 → 𝜃))) |
14 | 11, 12, 13 | 3bitr4i 305 |
. 2
⊢ (((𝑥 = 𝑦 → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ ∃𝑥(𝑥 = 𝑦 ∧ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))) ↔ (𝜃 ↔ 𝜏)) |
15 | 4, 14 | bitri 277 |
1
⊢ (𝜂 ↔ (𝜃 ↔ 𝜏)) |