Proof of Theorem mob
Step | Hyp | Ref
| Expression |
1 | | elex 2867 |
. . . . 5
⊢ (B ∈ D → B ∈ V) |
2 | | nfcv 2489 |
. . . . . . . 8
⊢
ℲxA |
3 | | nfv 1619 |
. . . . . . . . . 10
⊢ Ⅎx B ∈ V |
4 | | nfmo1 2215 |
. . . . . . . . . 10
⊢ Ⅎx∃*xφ |
5 | | nfv 1619 |
. . . . . . . . . 10
⊢ Ⅎxψ |
6 | 3, 4, 5 | nf3an 1827 |
. . . . . . . . 9
⊢ Ⅎx(B ∈ V ∧ ∃*xφ ∧ ψ) |
7 | | nfv 1619 |
. . . . . . . . 9
⊢ Ⅎx(A = B ↔ χ) |
8 | 6, 7 | nfim 1813 |
. . . . . . . 8
⊢ Ⅎx((B ∈ V ∧ ∃*xφ ∧ ψ) → (A = B ↔
χ)) |
9 | | moi.1 |
. . . . . . . . . 10
⊢ (x = A →
(φ ↔ ψ)) |
10 | 9 | 3anbi3d 1258 |
. . . . . . . . 9
⊢ (x = A →
((B ∈ V
∧ ∃*xφ ∧ φ) ↔ (B ∈ V ∧ ∃*xφ ∧ ψ))) |
11 | | eqeq1 2359 |
. . . . . . . . . 10
⊢ (x = A →
(x = B
↔ A = B)) |
12 | 11 | bibi1d 310 |
. . . . . . . . 9
⊢ (x = A →
((x = B
↔ χ) ↔ (A = B ↔
χ))) |
13 | 10, 12 | imbi12d 311 |
. . . . . . . 8
⊢ (x = A →
(((B ∈ V
∧ ∃*xφ ∧ φ) → (x = B ↔
χ)) ↔ ((B ∈ V ∧ ∃*xφ ∧ ψ) →
(A = B
↔ χ)))) |
14 | | moi.2 |
. . . . . . . . 9
⊢ (x = B →
(φ ↔ χ)) |
15 | 14 | mob2 3016 |
. . . . . . . 8
⊢ ((B ∈ V ∧ ∃*xφ ∧ φ) →
(x = B
↔ χ)) |
16 | 2, 8, 13, 15 | vtoclgf 2913 |
. . . . . . 7
⊢ (A ∈ C → ((B
∈ V ∧ ∃*xφ ∧ ψ) → (A = B ↔
χ))) |
17 | 16 | com12 27 |
. . . . . 6
⊢ ((B ∈ V ∧ ∃*xφ ∧ ψ) →
(A ∈
C → (A = B ↔
χ))) |
18 | 17 | 3expib 1154 |
. . . . 5
⊢ (B ∈ V →
((∃*xφ ∧ ψ) →
(A ∈
C → (A = B ↔
χ)))) |
19 | 1, 18 | syl 15 |
. . . 4
⊢ (B ∈ D → ((∃*xφ ∧ ψ) → (A ∈ C → (A =
B ↔ χ)))) |
20 | 19 | com3r 73 |
. . 3
⊢ (A ∈ C → (B
∈ D
→ ((∃*xφ ∧ ψ) →
(A = B
↔ χ)))) |
21 | 20 | imp 418 |
. 2
⊢ ((A ∈ C ∧ B ∈ D) → ((∃*xφ ∧ ψ) → (A = B ↔
χ))) |
22 | 21 | 3impib 1149 |
1
⊢ (((A ∈ C ∧ B ∈ D) ∧ ∃*xφ ∧ ψ) → (A = B ↔
χ)) |