Proof of Theorem sbanALT
Step | Hyp | Ref
| Expression |
1 | | biid 263 |
. . . 4
⊢ (((𝑥 = 𝑦 → (𝜑 → ¬ 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜑 → ¬ 𝜓))) ↔ ((𝑥 = 𝑦 → (𝜑 → ¬ 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜑 → ¬ 𝜓)))) |
2 | | biid 263 |
. . . 4
⊢ (((𝑥 = 𝑦 → ¬ (𝜑 → ¬ 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ ¬ (𝜑 → ¬ 𝜓))) ↔ ((𝑥 = 𝑦 → ¬ (𝜑 → ¬ 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ ¬ (𝜑 → ¬ 𝜓)))) |
3 | 1, 2 | sbnALT 2595 |
. . 3
⊢ (((𝑥 = 𝑦 → ¬ (𝜑 → ¬ 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ ¬ (𝜑 → ¬ 𝜓))) ↔ ¬ ((𝑥 = 𝑦 → (𝜑 → ¬ 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜑 → ¬ 𝜓)))) |
4 | | dfsb1.p6 |
. . . . 5
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) |
5 | | biid 263 |
. . . . 5
⊢ (((𝑥 = 𝑦 → ¬ 𝜓) ∧ ∃𝑥(𝑥 = 𝑦 ∧ ¬ 𝜓)) ↔ ((𝑥 = 𝑦 → ¬ 𝜓) ∧ ∃𝑥(𝑥 = 𝑦 ∧ ¬ 𝜓))) |
6 | 4, 5, 1 | sbimALT 2608 |
. . . 4
⊢ (((𝑥 = 𝑦 → (𝜑 → ¬ 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜑 → ¬ 𝜓))) ↔ (𝜃 → ((𝑥 = 𝑦 → ¬ 𝜓) ∧ ∃𝑥(𝑥 = 𝑦 ∧ ¬ 𝜓)))) |
7 | | dfsb1.s4 |
. . . . . 6
⊢ (𝜏 ↔ ((𝑥 = 𝑦 → 𝜓) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))) |
8 | 7, 5 | sbnALT 2595 |
. . . . 5
⊢ (((𝑥 = 𝑦 → ¬ 𝜓) ∧ ∃𝑥(𝑥 = 𝑦 ∧ ¬ 𝜓)) ↔ ¬ 𝜏) |
9 | 8 | imbi2i 338 |
. . . 4
⊢ ((𝜃 → ((𝑥 = 𝑦 → ¬ 𝜓) ∧ ∃𝑥(𝑥 = 𝑦 ∧ ¬ 𝜓))) ↔ (𝜃 → ¬ 𝜏)) |
10 | 6, 9 | bitri 277 |
. . 3
⊢ (((𝑥 = 𝑦 → (𝜑 → ¬ 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜑 → ¬ 𝜓))) ↔ (𝜃 → ¬ 𝜏)) |
11 | 3, 10 | xchbinx 336 |
. 2
⊢ (((𝑥 = 𝑦 → ¬ (𝜑 → ¬ 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ ¬ (𝜑 → ¬ 𝜓))) ↔ ¬ (𝜃 → ¬ 𝜏)) |
12 | | dfsb1.an |
. . 3
⊢ (𝜂 ↔ ((𝑥 = 𝑦 → (𝜑 ∧ 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜑 ∧ 𝜓)))) |
13 | | df-an 399 |
. . 3
⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)) |
14 | 12, 2, 13 | sbbiiALT 2578 |
. 2
⊢ (𝜂 ↔ ((𝑥 = 𝑦 → ¬ (𝜑 → ¬ 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ ¬ (𝜑 → ¬ 𝜓)))) |
15 | | df-an 399 |
. 2
⊢ ((𝜃 ∧ 𝜏) ↔ ¬ (𝜃 → ¬ 𝜏)) |
16 | 11, 14, 15 | 3bitr4i 305 |
1
⊢ (𝜂 ↔ (𝜃 ∧ 𝜏)) |