Proof of Theorem opm
Step | Hyp | Ref
| Expression |
1 | | df-op 3376 |
. . . . 5
⊢
〈A, B〉 = {x
∣ (A ∈ V ∧ B ∈ V ∧ x ∈ {{A},
{A, B}})} |
2 | 1 | eleq2i 2101 |
. . . 4
⊢ (x ∈ 〈A, B〉
↔ x ∈ {x ∣
(A ∈ V
∧ B ∈ V ∧ x ∈ {{A}, {A, B}})}) |
3 | 2 | exbii 1493 |
. . 3
⊢ (∃x x ∈ 〈A, B〉
↔ ∃x x ∈ {x ∣
(A ∈ V
∧ B ∈ V ∧ x ∈ {{A}, {A, B}})}) |
4 | | abid 2025 |
. . . 4
⊢ (x ∈ {x ∣ (A
∈ V ∧
B ∈ V
∧ x ∈ {{A},
{A, B}})} ↔ (A
∈ V ∧
B ∈ V
∧ x ∈ {{A},
{A, B}})) |
5 | 4 | exbii 1493 |
. . 3
⊢ (∃x x ∈ {x ∣ (A
∈ V ∧
B ∈ V
∧ x ∈ {{A},
{A, B}})} ↔ ∃x(A ∈ V ∧ B ∈ V ∧ x ∈ {{A}, {A, B}})) |
6 | 3, 5 | bitri 173 |
. 2
⊢ (∃x x ∈ 〈A, B〉
↔ ∃x(A ∈ V ∧ B ∈ V ∧ x ∈ {{A},
{A, B}})) |
7 | | 19.42v 1783 |
. . 3
⊢ (∃x((A ∈ V ∧ B ∈ V) ∧ x ∈ {{A}, {A, B}}) ↔ ((A
∈ V ∧
B ∈ V)
∧ ∃x x ∈ {{A},
{A, B}})) |
8 | | df-3an 886 |
. . . 4
⊢
((A ∈ V ∧ B ∈ V ∧ x ∈ {{A},
{A, B}}) ↔ ((A
∈ V ∧
B ∈ V)
∧ x ∈ {{A},
{A, B}})) |
9 | 8 | exbii 1493 |
. . 3
⊢ (∃x(A ∈ V ∧ B ∈ V ∧ x ∈ {{A}, {A, B}}) ↔ ∃x((A ∈ V ∧ B ∈ V) ∧ x ∈ {{A}, {A, B}})) |
10 | | df-3an 886 |
. . 3
⊢
((A ∈ V ∧ B ∈ V ∧ ∃x x ∈ {{A},
{A, B}}) ↔ ((A
∈ V ∧
B ∈ V)
∧ ∃x x ∈ {{A},
{A, B}})) |
11 | 7, 9, 10 | 3bitr4ri 202 |
. 2
⊢
((A ∈ V ∧ B ∈ V ∧ ∃x x ∈ {{A},
{A, B}}) ↔ ∃x(A ∈ V ∧ B ∈ V ∧ x ∈ {{A}, {A, B}})) |
12 | | 3simpa 900 |
. . 3
⊢
((A ∈ V ∧ B ∈ V ∧ ∃x x ∈ {{A},
{A, B}}) → (A
∈ V ∧
B ∈
V)) |
13 | | id 19 |
. . . 4
⊢
((A ∈ V ∧ B ∈ V) →
(A ∈ V
∧ B ∈ V)) |
14 | | snexgOLD 3926 |
. . . . . 6
⊢ (A ∈ V →
{A} ∈
V) |
15 | 14 | adantr 261 |
. . . . 5
⊢
((A ∈ V ∧ B ∈ V) →
{A} ∈
V) |
16 | | prmg 3480 |
. . . . 5
⊢
({A} ∈ V → ∃x x ∈ {{A}, {A, B}}) |
17 | 15, 16 | syl 14 |
. . . 4
⊢
((A ∈ V ∧ B ∈ V) →
∃x
x ∈
{{A}, {A, B}}) |
18 | 13, 17, 10 | sylanbrc 394 |
. . 3
⊢
((A ∈ V ∧ B ∈ V) →
(A ∈ V
∧ B ∈ V ∧ ∃x x ∈ {{A}, {A, B}})) |
19 | 12, 18 | impbii 117 |
. 2
⊢
((A ∈ V ∧ B ∈ V ∧ ∃x x ∈ {{A},
{A, B}}) ↔ (A
∈ V ∧
B ∈
V)) |
20 | 6, 11, 19 | 3bitr2i 197 |
1
⊢ (∃x x ∈ 〈A, B〉
↔ (A ∈ V ∧ B ∈
V)) |