Proof of Theorem reuprg
| Step | Hyp | Ref
| Expression |
| 1 | | reuprg.1 |
. . 3
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
| 2 | | reuprg.2 |
. . 3
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) |
| 3 | 1, 2 | reuprg0 4702 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃!𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ((𝜓 ∧ (𝜒 → 𝐴 = 𝐵)) ∨ (𝜒 ∧ (𝜓 → 𝐴 = 𝐵))))) |
| 4 | | orddi 1012 |
. . 3
⊢ (((𝜓 ∧ (𝜒 → 𝐴 = 𝐵)) ∨ (𝜒 ∧ (𝜓 → 𝐴 = 𝐵))) ↔ (((𝜓 ∨ 𝜒) ∧ (𝜓 ∨ (𝜓 → 𝐴 = 𝐵))) ∧ (((𝜒 → 𝐴 = 𝐵) ∨ 𝜒) ∧ ((𝜒 → 𝐴 = 𝐵) ∨ (𝜓 → 𝐴 = 𝐵))))) |
| 5 | | curryax 894 |
. . . . . 6
⊢ (𝜓 ∨ (𝜓 → 𝐴 = 𝐵)) |
| 6 | 5 | biantru 529 |
. . . . 5
⊢ ((𝜓 ∨ 𝜒) ↔ ((𝜓 ∨ 𝜒) ∧ (𝜓 ∨ (𝜓 → 𝐴 = 𝐵)))) |
| 7 | 6 | bicomi 224 |
. . . 4
⊢ (((𝜓 ∨ 𝜒) ∧ (𝜓 ∨ (𝜓 → 𝐴 = 𝐵))) ↔ (𝜓 ∨ 𝜒)) |
| 8 | | curryax 894 |
. . . . . . . 8
⊢ (𝜒 ∨ (𝜒 → 𝐴 = 𝐵)) |
| 9 | | orcom 871 |
. . . . . . . 8
⊢ (((𝜒 → 𝐴 = 𝐵) ∨ 𝜒) ↔ (𝜒 ∨ (𝜒 → 𝐴 = 𝐵))) |
| 10 | 8, 9 | mpbir 231 |
. . . . . . 7
⊢ ((𝜒 → 𝐴 = 𝐵) ∨ 𝜒) |
| 11 | 10 | biantrur 530 |
. . . . . 6
⊢ (((𝜒 → 𝐴 = 𝐵) ∨ (𝜓 → 𝐴 = 𝐵)) ↔ (((𝜒 → 𝐴 = 𝐵) ∨ 𝜒) ∧ ((𝜒 → 𝐴 = 𝐵) ∨ (𝜓 → 𝐴 = 𝐵)))) |
| 12 | 11 | bicomi 224 |
. . . . 5
⊢ ((((𝜒 → 𝐴 = 𝐵) ∨ 𝜒) ∧ ((𝜒 → 𝐴 = 𝐵) ∨ (𝜓 → 𝐴 = 𝐵))) ↔ ((𝜒 → 𝐴 = 𝐵) ∨ (𝜓 → 𝐴 = 𝐵))) |
| 13 | | pm4.79 1006 |
. . . . 5
⊢ (((𝜒 → 𝐴 = 𝐵) ∨ (𝜓 → 𝐴 = 𝐵)) ↔ ((𝜒 ∧ 𝜓) → 𝐴 = 𝐵)) |
| 14 | 12, 13 | bitri 275 |
. . . 4
⊢ ((((𝜒 → 𝐴 = 𝐵) ∨ 𝜒) ∧ ((𝜒 → 𝐴 = 𝐵) ∨ (𝜓 → 𝐴 = 𝐵))) ↔ ((𝜒 ∧ 𝜓) → 𝐴 = 𝐵)) |
| 15 | 7, 14 | anbi12i 628 |
. . 3
⊢ ((((𝜓 ∨ 𝜒) ∧ (𝜓 ∨ (𝜓 → 𝐴 = 𝐵))) ∧ (((𝜒 → 𝐴 = 𝐵) ∨ 𝜒) ∧ ((𝜒 → 𝐴 = 𝐵) ∨ (𝜓 → 𝐴 = 𝐵)))) ↔ ((𝜓 ∨ 𝜒) ∧ ((𝜒 ∧ 𝜓) → 𝐴 = 𝐵))) |
| 16 | 4, 15 | bitri 275 |
. 2
⊢ (((𝜓 ∧ (𝜒 → 𝐴 = 𝐵)) ∨ (𝜒 ∧ (𝜓 → 𝐴 = 𝐵))) ↔ ((𝜓 ∨ 𝜒) ∧ ((𝜒 ∧ 𝜓) → 𝐴 = 𝐵))) |
| 17 | 3, 16 | bitrdi 287 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃!𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ((𝜓 ∨ 𝜒) ∧ ((𝜒 ∧ 𝜓) → 𝐴 = 𝐵)))) |