Proof of Theorem mob
Step | Hyp | Ref
| Expression |
1 | | elex 3449 |
. . . . 5
⊢ (𝐵 ∈ 𝐷 → 𝐵 ∈ V) |
2 | | nfv 1917 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝐵 ∈ V |
3 | | nfmo1 2557 |
. . . . . . . . . 10
⊢
Ⅎ𝑥∃*𝑥𝜑 |
4 | | nfv 1917 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝜓 |
5 | 2, 3, 4 | nf3an 1904 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝐵 ∈ V ∧ ∃*𝑥𝜑 ∧ 𝜓) |
6 | | nfv 1917 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝐴 = 𝐵 ↔ 𝜒) |
7 | 5, 6 | nfim 1899 |
. . . . . . . 8
⊢
Ⅎ𝑥((𝐵 ∈ V ∧ ∃*𝑥𝜑 ∧ 𝜓) → (𝐴 = 𝐵 ↔ 𝜒)) |
8 | | moi.1 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
9 | 8 | 3anbi3d 1441 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ((𝐵 ∈ V ∧ ∃*𝑥𝜑 ∧ 𝜑) ↔ (𝐵 ∈ V ∧ ∃*𝑥𝜑 ∧ 𝜓))) |
10 | | eqeq1 2742 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝑥 = 𝐵 ↔ 𝐴 = 𝐵)) |
11 | 10 | bibi1d 344 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ((𝑥 = 𝐵 ↔ 𝜒) ↔ (𝐴 = 𝐵 ↔ 𝜒))) |
12 | 9, 11 | imbi12d 345 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (((𝐵 ∈ V ∧ ∃*𝑥𝜑 ∧ 𝜑) → (𝑥 = 𝐵 ↔ 𝜒)) ↔ ((𝐵 ∈ V ∧ ∃*𝑥𝜑 ∧ 𝜓) → (𝐴 = 𝐵 ↔ 𝜒)))) |
13 | | moi.2 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) |
14 | 13 | mob2 3651 |
. . . . . . . 8
⊢ ((𝐵 ∈ V ∧ ∃*𝑥𝜑 ∧ 𝜑) → (𝑥 = 𝐵 ↔ 𝜒)) |
15 | 7, 12, 14 | vtoclg1f 3503 |
. . . . . . 7
⊢ (𝐴 ∈ 𝐶 → ((𝐵 ∈ V ∧ ∃*𝑥𝜑 ∧ 𝜓) → (𝐴 = 𝐵 ↔ 𝜒))) |
16 | 15 | com12 32 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ ∃*𝑥𝜑 ∧ 𝜓) → (𝐴 ∈ 𝐶 → (𝐴 = 𝐵 ↔ 𝜒))) |
17 | 16 | 3expib 1121 |
. . . . 5
⊢ (𝐵 ∈ V → ((∃*𝑥𝜑 ∧ 𝜓) → (𝐴 ∈ 𝐶 → (𝐴 = 𝐵 ↔ 𝜒)))) |
18 | 1, 17 | syl 17 |
. . . 4
⊢ (𝐵 ∈ 𝐷 → ((∃*𝑥𝜑 ∧ 𝜓) → (𝐴 ∈ 𝐶 → (𝐴 = 𝐵 ↔ 𝜒)))) |
19 | 18 | com3r 87 |
. . 3
⊢ (𝐴 ∈ 𝐶 → (𝐵 ∈ 𝐷 → ((∃*𝑥𝜑 ∧ 𝜓) → (𝐴 = 𝐵 ↔ 𝜒)))) |
20 | 19 | imp 407 |
. 2
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ((∃*𝑥𝜑 ∧ 𝜓) → (𝐴 = 𝐵 ↔ 𝜒))) |
21 | 20 | 3impib 1115 |
1
⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∃*𝑥𝜑 ∧ 𝜓) → (𝐴 = 𝐵 ↔ 𝜒)) |