Step | Hyp | Ref
| Expression |
1 | | dfcleq 2171 |
. 2
⊢ ((V
∖ (V ∖ 𝐴)) =
𝐴 ↔ ∀𝑥(𝑥 ∈ (V ∖ (V ∖ 𝐴)) ↔ 𝑥 ∈ 𝐴)) |
2 | | eldif 3138 |
. . . . . . 7
⊢ (𝑥 ∈ (V ∖ (V ∖
𝐴)) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ (V ∖ 𝐴))) |
3 | | vex 2740 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
4 | 3 | biantrur 303 |
. . . . . . 7
⊢ (¬
𝑥 ∈ (V ∖ 𝐴) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ (V ∖ 𝐴))) |
5 | | eldif 3138 |
. . . . . . . . 9
⊢ (𝑥 ∈ (V ∖ 𝐴) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ 𝐴)) |
6 | 3 | biantrur 303 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ 𝐴 ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ 𝐴)) |
7 | 5, 6 | bitr4i 187 |
. . . . . . . 8
⊢ (𝑥 ∈ (V ∖ 𝐴) ↔ ¬ 𝑥 ∈ 𝐴) |
8 | 7 | notbii 668 |
. . . . . . 7
⊢ (¬
𝑥 ∈ (V ∖ 𝐴) ↔ ¬ ¬ 𝑥 ∈ 𝐴) |
9 | 2, 4, 8 | 3bitr2i 208 |
. . . . . 6
⊢ (𝑥 ∈ (V ∖ (V ∖
𝐴)) ↔ ¬ ¬
𝑥 ∈ 𝐴) |
10 | 9 | bibi1i 228 |
. . . . 5
⊢ ((𝑥 ∈ (V ∖ (V ∖
𝐴)) ↔ 𝑥 ∈ 𝐴) ↔ (¬ ¬ 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)) |
11 | | biimp 118 |
. . . . . 6
⊢ ((¬
¬ 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴) → (¬ ¬ 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)) |
12 | | id 19 |
. . . . . . 7
⊢ ((¬
¬ 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴) → (¬ ¬ 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)) |
13 | | notnot 629 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → ¬ ¬ 𝑥 ∈ 𝐴) |
14 | 12, 13 | impbid1 142 |
. . . . . 6
⊢ ((¬
¬ 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴) → (¬ ¬ 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)) |
15 | 11, 14 | impbii 126 |
. . . . 5
⊢ ((¬
¬ 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴) ↔ (¬ ¬ 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)) |
16 | 10, 15 | bitri 184 |
. . . 4
⊢ ((𝑥 ∈ (V ∖ (V ∖
𝐴)) ↔ 𝑥 ∈ 𝐴) ↔ (¬ ¬ 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)) |
17 | | df-stab 831 |
. . . 4
⊢
(STAB 𝑥 ∈ 𝐴 ↔ (¬ ¬ 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)) |
18 | 16, 17 | bitr4i 187 |
. . 3
⊢ ((𝑥 ∈ (V ∖ (V ∖
𝐴)) ↔ 𝑥 ∈ 𝐴) ↔ STAB 𝑥 ∈ 𝐴) |
19 | 18 | albii 1470 |
. 2
⊢
(∀𝑥(𝑥 ∈ (V ∖ (V ∖
𝐴)) ↔ 𝑥 ∈ 𝐴) ↔ ∀𝑥STAB 𝑥 ∈ 𝐴) |
20 | 1, 19 | bitri 184 |
1
⊢ ((V
∖ (V ∖ 𝐴)) =
𝐴 ↔ ∀𝑥STAB 𝑥 ∈ 𝐴) |