Step | Hyp | Ref
| Expression |
1 | | anandir 525 |
. . . . . . . 8
⊢
(((x ∈ A ∧ ¬ x ∈ B) ∧ x𝐹y) ↔ ((x
∈ A ∧ x𝐹y) ∧ (¬
x ∈
B ∧
x𝐹y))) |
2 | 1 | exbii 1493 |
. . . . . . 7
⊢ (∃x((x ∈ A ∧ ¬ x ∈ B) ∧ x𝐹y)
↔ ∃x((x ∈ A ∧ x𝐹y) ∧ (¬
x ∈
B ∧
x𝐹y))) |
3 | | 19.40 1519 |
. . . . . . 7
⊢ (∃x((x ∈ A ∧ x𝐹y) ∧ (¬ x ∈ B ∧ x𝐹y)) → (∃x(x ∈ A ∧ x𝐹y) ∧ ∃x(¬ x ∈ B ∧ x𝐹y))) |
4 | 2, 3 | sylbi 114 |
. . . . . 6
⊢ (∃x((x ∈ A ∧ ¬ x ∈ B) ∧ x𝐹y)
→ (∃x(x ∈ A ∧ x𝐹y) ∧ ∃x(¬
x ∈
B ∧
x𝐹y))) |
5 | | nfv 1418 |
. . . . . . . . . . 11
⊢
ℲxFun ◡𝐹 |
6 | | nfe1 1382 |
. . . . . . . . . . 11
⊢
Ⅎx∃x(x𝐹y ∧ ¬ x ∈ B) |
7 | 5, 6 | nfan 1454 |
. . . . . . . . . 10
⊢
Ⅎx(Fun ◡𝐹 ∧ ∃x(x𝐹y ∧ ¬ x ∈ B)) |
8 | | funmo 4860 |
. . . . . . . . . . . . . 14
⊢ (Fun
◡𝐹 → ∃*x y◡𝐹x) |
9 | | vex 2554 |
. . . . . . . . . . . . . . . 16
⊢ y ∈
V |
10 | | vex 2554 |
. . . . . . . . . . . . . . . 16
⊢ x ∈
V |
11 | 9, 10 | brcnv 4461 |
. . . . . . . . . . . . . . 15
⊢ (y◡𝐹x ↔ x𝐹y) |
12 | 11 | mobii 1934 |
. . . . . . . . . . . . . 14
⊢ (∃*x y◡𝐹x ↔ ∃*x x𝐹y) |
13 | 8, 12 | sylib 127 |
. . . . . . . . . . . . 13
⊢ (Fun
◡𝐹 → ∃*x x𝐹y) |
14 | | mopick 1975 |
. . . . . . . . . . . . 13
⊢ ((∃*x x𝐹y ∧ ∃x(x𝐹y ∧ ¬ x ∈ B)) → (x𝐹y →
¬ x ∈
B)) |
15 | 13, 14 | sylan 267 |
. . . . . . . . . . . 12
⊢ ((Fun
◡𝐹 ∧ ∃x(x𝐹y ∧ ¬ x ∈ B)) →
(x𝐹y →
¬ x ∈
B)) |
16 | 15 | con2d 554 |
. . . . . . . . . . 11
⊢ ((Fun
◡𝐹 ∧ ∃x(x𝐹y ∧ ¬ x ∈ B)) →
(x ∈
B → ¬ x𝐹y)) |
17 | | imnan 623 |
. . . . . . . . . . 11
⊢
((x ∈ B →
¬ x𝐹y)
↔ ¬ (x ∈ B ∧ x𝐹y)) |
18 | 16, 17 | sylib 127 |
. . . . . . . . . 10
⊢ ((Fun
◡𝐹 ∧ ∃x(x𝐹y ∧ ¬ x ∈ B)) →
¬ (x ∈ B ∧ x𝐹y)) |
19 | 7, 18 | alrimi 1412 |
. . . . . . . . 9
⊢ ((Fun
◡𝐹 ∧ ∃x(x𝐹y ∧ ¬ x ∈ B)) →
∀x
¬ (x ∈ B ∧ x𝐹y)) |
20 | 19 | ex 108 |
. . . . . . . 8
⊢ (Fun
◡𝐹 → (∃x(x𝐹y ∧ ¬ x ∈ B) →
∀x
¬ (x ∈ B ∧ x𝐹y))) |
21 | | exancom 1496 |
. . . . . . . 8
⊢ (∃x(x𝐹y ∧ ¬ x ∈ B) ↔
∃x(¬
x ∈
B ∧
x𝐹y)) |
22 | | alnex 1385 |
. . . . . . . 8
⊢ (∀x ¬
(x ∈
B ∧
x𝐹y)
↔ ¬ ∃x(x ∈ B ∧ x𝐹y)) |
23 | 20, 21, 22 | 3imtr3g 193 |
. . . . . . 7
⊢ (Fun
◡𝐹 → (∃x(¬
x ∈
B ∧
x𝐹y)
→ ¬ ∃x(x ∈ B ∧ x𝐹y))) |
24 | 23 | anim2d 320 |
. . . . . 6
⊢ (Fun
◡𝐹 → ((∃x(x ∈ A ∧ x𝐹y) ∧ ∃x(¬ x ∈ B ∧ x𝐹y)) → (∃x(x ∈ A ∧ x𝐹y) ∧ ¬ ∃x(x ∈ B ∧ x𝐹y)))) |
25 | 4, 24 | syl5 28 |
. . . . 5
⊢ (Fun
◡𝐹 → (∃x((x ∈ A ∧ ¬ x ∈ B) ∧ x𝐹y)
→ (∃x(x ∈ A ∧ x𝐹y) ∧ ¬ ∃x(x ∈ B ∧ x𝐹y)))) |
26 | | df-rex 2306 |
. . . . . 6
⊢ (∃x ∈ (A ∖
B)x𝐹y ↔
∃x(x ∈ (A ∖
B) ∧
x𝐹y)) |
27 | | eldif 2921 |
. . . . . . . 8
⊢ (x ∈ (A ∖ B)
↔ (x ∈ A ∧ ¬ x ∈ B)) |
28 | 27 | anbi1i 431 |
. . . . . . 7
⊢
((x ∈ (A ∖
B) ∧
x𝐹y)
↔ ((x ∈ A ∧ ¬ x ∈ B) ∧ x𝐹y)) |
29 | 28 | exbii 1493 |
. . . . . 6
⊢ (∃x(x ∈ (A ∖ B)
∧ x𝐹y) ↔ ∃x((x ∈ A ∧ ¬ x ∈ B) ∧ x𝐹y)) |
30 | 26, 29 | bitri 173 |
. . . . 5
⊢ (∃x ∈ (A ∖
B)x𝐹y ↔
∃x((x ∈ A ∧ ¬ x ∈ B) ∧ x𝐹y)) |
31 | | df-rex 2306 |
. . . . . 6
⊢ (∃x ∈ A x𝐹y ↔
∃x(x ∈ A ∧ x𝐹y)) |
32 | | df-rex 2306 |
. . . . . . 7
⊢ (∃x ∈ B x𝐹y ↔
∃x(x ∈ B ∧ x𝐹y)) |
33 | 32 | notbii 593 |
. . . . . 6
⊢ (¬
∃x ∈ B x𝐹y ↔
¬ ∃x(x ∈ B ∧ x𝐹y)) |
34 | 31, 33 | anbi12i 433 |
. . . . 5
⊢ ((∃x ∈ A x𝐹y ∧ ¬ ∃x ∈ B x𝐹y) ↔ (∃x(x ∈ A ∧ x𝐹y) ∧ ¬ ∃x(x ∈ B ∧ x𝐹y))) |
35 | 25, 30, 34 | 3imtr4g 194 |
. . . 4
⊢ (Fun
◡𝐹 → (∃x ∈ (A ∖
B)x𝐹y →
(∃x
∈ A
x𝐹y ∧ ¬ ∃x ∈ B x𝐹y))) |
36 | 35 | ss2abdv 3007 |
. . 3
⊢ (Fun
◡𝐹 → {y ∣ ∃x ∈ (A ∖
B)x𝐹y}
⊆ {y ∣ (∃x ∈ A x𝐹y ∧ ¬ ∃x ∈ B x𝐹y)}) |
37 | | dfima2 4613 |
. . 3
⊢ (𝐹 “ (A ∖ B)) =
{y ∣ ∃x ∈ (A ∖
B)x𝐹y} |
38 | | dfima2 4613 |
. . . . 5
⊢ (𝐹 “ A) = {y ∣
∃x ∈ A x𝐹y} |
39 | | dfima2 4613 |
. . . . 5
⊢ (𝐹 “ B) = {y ∣
∃x ∈ B x𝐹y} |
40 | 38, 39 | difeq12i 3054 |
. . . 4
⊢ ((𝐹 “ A) ∖ (𝐹 “ B)) = ({y
∣ ∃x ∈ A x𝐹y} ∖ {y
∣ ∃x ∈ B x𝐹y}) |
41 | | difab 3200 |
. . . 4
⊢
({y ∣ ∃x ∈ A x𝐹y}
∖ {y ∣ ∃x ∈ B x𝐹y}) =
{y ∣ (∃x ∈ A x𝐹y ∧ ¬ ∃x ∈ B x𝐹y)} |
42 | 40, 41 | eqtri 2057 |
. . 3
⊢ ((𝐹 “ A) ∖ (𝐹 “ B)) = {y ∣
(∃x
∈ A
x𝐹y ∧ ¬ ∃x ∈ B x𝐹y)} |
43 | 36, 37, 42 | 3sstr4g 2980 |
. 2
⊢ (Fun
◡𝐹 → (𝐹 “ (A ∖ B))
⊆ ((𝐹 “
A) ∖ (𝐹 “ B))) |
44 | | imadiflem 4921 |
. . 3
⊢ ((𝐹 “ A) ∖ (𝐹 “ B)) ⊆ (𝐹 “ (A ∖ B)) |
45 | 44 | a1i 9 |
. 2
⊢ (Fun
◡𝐹 → ((𝐹 “ A) ∖ (𝐹 “ B)) ⊆ (𝐹 “ (A ∖ B))) |
46 | 43, 45 | eqssd 2956 |
1
⊢ (Fun
◡𝐹 → (𝐹 “ (A ∖ B)) =
((𝐹 “ A) ∖ (𝐹 “ B))) |