Step | Hyp | Ref
| Expression |
1 | | df-ima 5573 |
. . . . . . 7
⊢ (𝐹 “ 𝐵) = ran (𝐹 ↾ 𝐵) |
2 | | mptsnun.f |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥}) |
3 | 2 | reseq1i 5856 |
. . . . . . . . . 10
⊢ (𝐹 ↾ 𝐵) = ((𝑥 ∈ 𝐴 ↦ {𝑥}) ↾ 𝐵) |
4 | | resmpt 5914 |
. . . . . . . . . 10
⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ {𝑥}) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ {𝑥})) |
5 | 3, 4 | syl5eq 2791 |
. . . . . . . . 9
⊢ (𝐵 ⊆ 𝐴 → (𝐹 ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ {𝑥})) |
6 | 5 | rneqd 5816 |
. . . . . . . 8
⊢ (𝐵 ⊆ 𝐴 → ran (𝐹 ↾ 𝐵) = ran (𝑥 ∈ 𝐵 ↦ {𝑥})) |
7 | | rnmptsn 35256 |
. . . . . . . 8
⊢ ran
(𝑥 ∈ 𝐵 ↦ {𝑥}) = {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}} |
8 | 6, 7 | eqtrdi 2795 |
. . . . . . 7
⊢ (𝐵 ⊆ 𝐴 → ran (𝐹 ↾ 𝐵) = {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) |
9 | 1, 8 | syl5eq 2791 |
. . . . . 6
⊢ (𝐵 ⊆ 𝐴 → (𝐹 “ 𝐵) = {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) |
10 | 9 | unieqd 4842 |
. . . . 5
⊢ (𝐵 ⊆ 𝐴 → ∪ (𝐹 “ 𝐵) = ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) |
11 | 10 | eleq2d 2824 |
. . . 4
⊢ (𝐵 ⊆ 𝐴 → (𝑥 ∈ ∪ (𝐹 “ 𝐵) ↔ 𝑥 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
12 | | eleq1w 2821 |
. . . . . 6
⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵)) |
13 | | eluniab 4843 |
. . . . . . . . 9
⊢ (𝑧 ∈ ∪ {𝑢
∣ ∃𝑥 ∈
𝐵 𝑢 = {𝑥}} ↔ ∃𝑢(𝑧 ∈ 𝑢 ∧ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥})) |
14 | | ancom 464 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝑢 ∧ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}) ↔ (∃𝑥 ∈ 𝐵 𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢)) |
15 | | r19.41v 3267 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
𝐵 (𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢) ↔ (∃𝑥 ∈ 𝐵 𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢)) |
16 | | df-rex 3068 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
𝐵 (𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢))) |
17 | 14, 15, 16 | 3bitr2i 302 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑢 ∧ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢))) |
18 | | eleq2 2827 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = {𝑥} → (𝑧 ∈ 𝑢 ↔ 𝑧 ∈ {𝑥})) |
19 | 18 | anbi2d 632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = {𝑥} → ((𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢) ↔ (𝑢 = {𝑥} ∧ 𝑧 ∈ {𝑥}))) |
20 | 19 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢) → ((𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢) ↔ (𝑢 = {𝑥} ∧ 𝑧 ∈ {𝑥}))) |
21 | 20 | ibi 270 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢) → (𝑢 = {𝑥} ∧ 𝑧 ∈ {𝑥})) |
22 | 21 | anim2i 620 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐵 ∧ (𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢)) → (𝑥 ∈ 𝐵 ∧ (𝑢 = {𝑥} ∧ 𝑧 ∈ {𝑥}))) |
23 | 22 | eximi 1842 |
. . . . . . . . . . . 12
⊢
(∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢)) → ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑢 = {𝑥} ∧ 𝑧 ∈ {𝑥}))) |
24 | 17, 23 | sylbi 220 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑢 ∧ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}) → ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑢 = {𝑥} ∧ 𝑧 ∈ {𝑥}))) |
25 | | an12 645 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐵 ∧ (𝑢 = {𝑥} ∧ 𝑧 ∈ {𝑥})) ↔ (𝑢 = {𝑥} ∧ (𝑥 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}))) |
26 | 25 | exbii 1855 |
. . . . . . . . . . . 12
⊢
(∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑢 = {𝑥} ∧ 𝑧 ∈ {𝑥})) ↔ ∃𝑥(𝑢 = {𝑥} ∧ (𝑥 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}))) |
27 | | exsimpr 1877 |
. . . . . . . . . . . 12
⊢
(∃𝑥(𝑢 = {𝑥} ∧ (𝑥 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) |
28 | 26, 27 | sylbi 220 |
. . . . . . . . . . 11
⊢
(∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑢 = {𝑥} ∧ 𝑧 ∈ {𝑥})) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) |
29 | 24, 28 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑢 ∧ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) |
30 | 29 | exlimiv 1938 |
. . . . . . . . 9
⊢
(∃𝑢(𝑧 ∈ 𝑢 ∧ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) |
31 | 13, 30 | sylbi 220 |
. . . . . . . 8
⊢ (𝑧 ∈ ∪ {𝑢
∣ ∃𝑥 ∈
𝐵 𝑢 = {𝑥}} → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) |
32 | | velsn 4566 |
. . . . . . . . . 10
⊢ (𝑧 ∈ {𝑥} ↔ 𝑧 = 𝑥) |
33 | 32 | anbi2i 626 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ↔ (𝑥 ∈ 𝐵 ∧ 𝑧 = 𝑥)) |
34 | 33 | exbii 1855 |
. . . . . . . 8
⊢
(∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑧 = 𝑥)) |
35 | 31, 34 | sylib 221 |
. . . . . . 7
⊢ (𝑧 ∈ ∪ {𝑢
∣ ∃𝑥 ∈
𝐵 𝑢 = {𝑥}} → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑧 = 𝑥)) |
36 | 12 | biimparc 483 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑧 = 𝑥) → 𝑧 ∈ 𝐵) |
37 | 36 | exlimiv 1938 |
. . . . . . 7
⊢
(∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑧 = 𝑥) → 𝑧 ∈ 𝐵) |
38 | 35, 37 | syl 17 |
. . . . . 6
⊢ (𝑧 ∈ ∪ {𝑢
∣ ∃𝑥 ∈
𝐵 𝑢 = {𝑥}} → 𝑧 ∈ 𝐵) |
39 | 12, 38 | vtoclga 3496 |
. . . . 5
⊢ (𝑥 ∈ ∪ {𝑢
∣ ∃𝑥 ∈
𝐵 𝑢 = {𝑥}} → 𝑥 ∈ 𝐵) |
40 | | equid 2020 |
. . . . . 6
⊢ 𝑥 = 𝑥 |
41 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ {𝑥} = {𝑥} |
42 | | snex 5333 |
. . . . . . . . . . . . . 14
⊢ {𝑥} ∈ V |
43 | | sbcg 3783 |
. . . . . . . . . . . . . 14
⊢ ({𝑥} ∈ V →
([{𝑥} / 𝑢]𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵)) |
44 | 42, 43 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
([{𝑥} / 𝑢]𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵) |
45 | | eqsbc3 3752 |
. . . . . . . . . . . . . 14
⊢ ({𝑥} ∈ V →
([{𝑥} / 𝑢]𝑢 = {𝑥} ↔ {𝑥} = {𝑥})) |
46 | 42, 45 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
([{𝑥} / 𝑢]𝑢 = {𝑥} ↔ {𝑥} = {𝑥}) |
47 | 18 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → (𝑧 ∈ 𝑢 ↔ 𝑧 ∈ {𝑥})) |
48 | | df-rex 3068 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑥 ∈
𝐵 𝑢 = {𝑥} ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥})) |
49 | 13 | biimpri 231 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∃𝑢(𝑧 ∈ 𝑢 ∧ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}) → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) |
50 | 49 | 19.23bi 2189 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ 𝑢 ∧ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}) → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) |
51 | 50 | expcom 417 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑥 ∈
𝐵 𝑢 = {𝑥} → (𝑧 ∈ 𝑢 → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
52 | 48, 51 | sylbir 238 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → (𝑧 ∈ 𝑢 → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
53 | 52 | 19.23bi 2189 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → (𝑧 ∈ 𝑢 → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
54 | 47, 53 | sylbird 263 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → (𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
55 | 54 | sbcth 3718 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑥} ∈ V → [{𝑥} / 𝑢]((𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → (𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}))) |
56 | 42, 55 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
[{𝑥} / 𝑢]((𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → (𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
57 | | sbcimg 3754 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑥} ∈ V →
([{𝑥} / 𝑢]((𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → (𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) ↔ ([{𝑥} / 𝑢](𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → [{𝑥} / 𝑢](𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})))) |
58 | 42, 57 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
([{𝑥} / 𝑢]((𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → (𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) ↔ ([{𝑥} / 𝑢](𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → [{𝑥} / 𝑢](𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}))) |
59 | 56, 58 | mpbi 233 |
. . . . . . . . . . . . . 14
⊢
([{𝑥} / 𝑢](𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → [{𝑥} / 𝑢](𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
60 | | sbcan 3755 |
. . . . . . . . . . . . . 14
⊢
([{𝑥} / 𝑢](𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) ↔ ([{𝑥} / 𝑢]𝑥 ∈ 𝐵 ∧ [{𝑥} / 𝑢]𝑢 = {𝑥})) |
61 | | nfv 1922 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑢 𝑧 ∈ {𝑥} |
62 | | nfab1 2907 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑢{𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}} |
63 | 62 | nfuni 4835 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑢∪ {𝑢
∣ ∃𝑥 ∈
𝐵 𝑢 = {𝑥}} |
64 | 63 | nfcri 2892 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑢 𝑧 ∈ ∪ {𝑢
∣ ∃𝑥 ∈
𝐵 𝑢 = {𝑥}} |
65 | 61, 64 | nfim 1904 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑢(𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) |
66 | 42, 65 | sbcgfi 3785 |
. . . . . . . . . . . . . 14
⊢
([{𝑥} / 𝑢](𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) ↔ (𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
67 | 59, 60, 66 | 3imtr3i 294 |
. . . . . . . . . . . . 13
⊢
(([{𝑥} /
𝑢]𝑥 ∈ 𝐵 ∧ [{𝑥} / 𝑢]𝑢 = {𝑥}) → (𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
68 | 44, 46, 67 | syl2anbr 602 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐵 ∧ {𝑥} = {𝑥}) → (𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
69 | 41, 68 | mpan2 691 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐵 → (𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
70 | 32, 69 | syl5bir 246 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐵 → (𝑧 = 𝑥 → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
71 | | eleq1w 2821 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → (𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}} ↔ 𝑥 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
72 | 70, 71 | mpbidi 244 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → (𝑧 = 𝑥 → 𝑥 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
73 | 72 | com12 32 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
74 | 73 | sbimi 2081 |
. . . . . . 7
⊢ ([𝑥 / 𝑧]𝑧 = 𝑥 → [𝑥 / 𝑧](𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
75 | | equsb3 2106 |
. . . . . . 7
⊢ ([𝑥 / 𝑧]𝑧 = 𝑥 ↔ 𝑥 = 𝑥) |
76 | | sbv 2095 |
. . . . . . 7
⊢ ([𝑥 / 𝑧](𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) ↔ (𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
77 | 74, 75, 76 | 3imtr3i 294 |
. . . . . 6
⊢ (𝑥 = 𝑥 → (𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
78 | 40, 77 | ax-mp 5 |
. . . . 5
⊢ (𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) |
79 | 39, 78 | impbii 212 |
. . . 4
⊢ (𝑥 ∈ ∪ {𝑢
∣ ∃𝑥 ∈
𝐵 𝑢 = {𝑥}} ↔ 𝑥 ∈ 𝐵) |
80 | 11, 79 | bitrdi 290 |
. . 3
⊢ (𝐵 ⊆ 𝐴 → (𝑥 ∈ ∪ (𝐹 “ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
81 | 80 | eqrdv 2736 |
. 2
⊢ (𝐵 ⊆ 𝐴 → ∪ (𝐹 “ 𝐵) = 𝐵) |
82 | 81 | eqcomd 2744 |
1
⊢ (𝐵 ⊆ 𝐴 → 𝐵 = ∪ (𝐹 “ 𝐵)) |