Proof of Theorem dfdif3
Step | Hyp | Ref
| Expression |
1 | | dfdif2 3110 |
. 2
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐵} |
2 | | a9ev 1677 |
. . . . . . 7
⊢
∃𝑦 𝑦 = 𝑥 |
3 | 2 | biantrur 301 |
. . . . . 6
⊢ (¬
𝑥 ∈ 𝐵 ↔ (∃𝑦 𝑦 = 𝑥 ∧ ¬ 𝑥 ∈ 𝐵)) |
4 | | 19.41v 1882 |
. . . . . 6
⊢
(∃𝑦(𝑦 = 𝑥 ∧ ¬ 𝑥 ∈ 𝐵) ↔ (∃𝑦 𝑦 = 𝑥 ∧ ¬ 𝑥 ∈ 𝐵)) |
5 | 3, 4 | bitr4i 186 |
. . . . 5
⊢ (¬
𝑥 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝑥 ∧ ¬ 𝑥 ∈ 𝐵)) |
6 | | sb56 1865 |
. . . . 5
⊢
(∃𝑦(𝑦 = 𝑥 ∧ ¬ 𝑥 ∈ 𝐵) ↔ ∀𝑦(𝑦 = 𝑥 → ¬ 𝑥 ∈ 𝐵)) |
7 | | equcom 1686 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦) |
8 | 7 | imbi1i 237 |
. . . . . . 7
⊢ ((𝑦 = 𝑥 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 = 𝑦 → ¬ 𝑥 ∈ 𝐵)) |
9 | | eleq1w 2218 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
10 | 9 | notbid 657 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (¬ 𝑥 ∈ 𝐵 ↔ ¬ 𝑦 ∈ 𝐵)) |
11 | 10 | pm5.74i 179 |
. . . . . . . 8
⊢ ((𝑥 = 𝑦 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 = 𝑦 → ¬ 𝑦 ∈ 𝐵)) |
12 | | con2b 659 |
. . . . . . . 8
⊢ ((𝑥 = 𝑦 → ¬ 𝑦 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 → ¬ 𝑥 = 𝑦)) |
13 | | df-ne 2328 |
. . . . . . . . . 10
⊢ (𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦) |
14 | 13 | bicomi 131 |
. . . . . . . . 9
⊢ (¬
𝑥 = 𝑦 ↔ 𝑥 ≠ 𝑦) |
15 | 14 | imbi2i 225 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐵 → ¬ 𝑥 = 𝑦) ↔ (𝑦 ∈ 𝐵 → 𝑥 ≠ 𝑦)) |
16 | 11, 12, 15 | 3bitri 205 |
. . . . . . 7
⊢ ((𝑥 = 𝑦 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 → 𝑥 ≠ 𝑦)) |
17 | 8, 16 | bitri 183 |
. . . . . 6
⊢ ((𝑦 = 𝑥 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 → 𝑥 ≠ 𝑦)) |
18 | 17 | albii 1450 |
. . . . 5
⊢
(∀𝑦(𝑦 = 𝑥 → ¬ 𝑥 ∈ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ≠ 𝑦)) |
19 | 5, 6, 18 | 3bitri 205 |
. . . 4
⊢ (¬
𝑥 ∈ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ≠ 𝑦)) |
20 | | df-ral 2440 |
. . . 4
⊢
(∀𝑦 ∈
𝐵 𝑥 ≠ 𝑦 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ≠ 𝑦)) |
21 | 19, 20 | bitr4i 186 |
. . 3
⊢ (¬
𝑥 ∈ 𝐵 ↔ ∀𝑦 ∈ 𝐵 𝑥 ≠ 𝑦) |
22 | 21 | rabbii 2698 |
. 2
⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐵} = {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 𝑥 ≠ 𝑦} |
23 | 1, 22 | eqtri 2178 |
1
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 𝑥 ≠ 𝑦} |