Proof of Theorem 2mos
Step | Hyp | Ref
| Expression |
1 | | 2mo 2651 |
. 2
⊢
(∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
2 | | nfv 1920 |
. . . . . . . . . 10
⊢
Ⅎ𝑦 𝑥 = 𝑧 |
3 | 2 | sbrim 2304 |
. . . . . . . . 9
⊢ ([𝑤 / 𝑦](𝑥 = 𝑧 → 𝜑) ↔ (𝑥 = 𝑧 → [𝑤 / 𝑦]𝜑)) |
4 | | 2mos.1 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) |
5 | 4 | expcom 413 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑤 → (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))) |
6 | 5 | pm5.74d 272 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑤 → ((𝑥 = 𝑧 → 𝜑) ↔ (𝑥 = 𝑧 → 𝜓))) |
7 | 6 | sbievw 2098 |
. . . . . . . . 9
⊢ ([𝑤 / 𝑦](𝑥 = 𝑧 → 𝜑) ↔ (𝑥 = 𝑧 → 𝜓)) |
8 | 3, 7 | bitr3i 276 |
. . . . . . . 8
⊢ ((𝑥 = 𝑧 → [𝑤 / 𝑦]𝜑) ↔ (𝑥 = 𝑧 → 𝜓)) |
9 | 8 | pm5.74ri 271 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ([𝑤 / 𝑦]𝜑 ↔ 𝜓)) |
10 | 9 | sbievw 2098 |
. . . . . 6
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ 𝜓) |
11 | 10 | anbi2i 622 |
. . . . 5
⊢ ((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) ↔ (𝜑 ∧ 𝜓)) |
12 | 11 | imbi1i 349 |
. . . 4
⊢ (((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ((𝜑 ∧ 𝜓) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
13 | 12 | 2albii 1826 |
. . 3
⊢
(∀𝑧∀𝑤((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
14 | 13 | 2albii 1826 |
. 2
⊢
(∀𝑥∀𝑦∀𝑧∀𝑤((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
15 | 1, 14 | bitri 274 |
1
⊢
(∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |