Step | Hyp | Ref
| Expression |
1 | | df-ima 5267 |
. . . . . . 7
⊢ (𝐹 “ 𝐵) = ran (𝐹 ↾ 𝐵) |
2 | | mptsnun.f |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥}) |
3 | 2 | reseq1i 5535 |
. . . . . . . . . 10
⊢ (𝐹 ↾ 𝐵) = ((𝑥 ∈ 𝐴 ↦ {𝑥}) ↾ 𝐵) |
4 | | resmpt 5595 |
. . . . . . . . . 10
⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ {𝑥}) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ {𝑥})) |
5 | 3, 4 | syl5eq 2794 |
. . . . . . . . 9
⊢ (𝐵 ⊆ 𝐴 → (𝐹 ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ {𝑥})) |
6 | 5 | rneqd 5496 |
. . . . . . . 8
⊢ (𝐵 ⊆ 𝐴 → ran (𝐹 ↾ 𝐵) = ran (𝑥 ∈ 𝐵 ↦ {𝑥})) |
7 | | rnmptsn 33464 |
. . . . . . . 8
⊢ ran
(𝑥 ∈ 𝐵 ↦ {𝑥}) = {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}} |
8 | 6, 7 | syl6eq 2798 |
. . . . . . 7
⊢ (𝐵 ⊆ 𝐴 → ran (𝐹 ↾ 𝐵) = {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) |
9 | 1, 8 | syl5eq 2794 |
. . . . . 6
⊢ (𝐵 ⊆ 𝐴 → (𝐹 “ 𝐵) = {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) |
10 | 9 | unieqd 4586 |
. . . . 5
⊢ (𝐵 ⊆ 𝐴 → ∪ (𝐹 “ 𝐵) = ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) |
11 | 10 | eleq2d 2813 |
. . . 4
⊢ (𝐵 ⊆ 𝐴 → (𝑥 ∈ ∪ (𝐹 “ 𝐵) ↔ 𝑥 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
12 | | eleq1 2815 |
. . . . . 6
⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵)) |
13 | | eluniab 4587 |
. . . . . . . . 9
⊢ (𝑧 ∈ ∪ {𝑢
∣ ∃𝑥 ∈
𝐵 𝑢 = {𝑥}} ↔ ∃𝑢(𝑧 ∈ 𝑢 ∧ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥})) |
14 | | ancom 465 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝑢 ∧ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}) ↔ (∃𝑥 ∈ 𝐵 𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢)) |
15 | | r19.41v 3215 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
𝐵 (𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢) ↔ (∃𝑥 ∈ 𝐵 𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢)) |
16 | | df-rex 3044 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
𝐵 (𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢))) |
17 | 14, 15, 16 | 3bitr2i 288 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑢 ∧ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢))) |
18 | | eleq2 2816 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = {𝑥} → (𝑧 ∈ 𝑢 ↔ 𝑧 ∈ {𝑥})) |
19 | 18 | anbi2d 742 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = {𝑥} → ((𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢) ↔ (𝑢 = {𝑥} ∧ 𝑧 ∈ {𝑥}))) |
20 | 19 | adantr 472 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢) → ((𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢) ↔ (𝑢 = {𝑥} ∧ 𝑧 ∈ {𝑥}))) |
21 | 20 | ibi 256 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢) → (𝑢 = {𝑥} ∧ 𝑧 ∈ {𝑥})) |
22 | 21 | anim2i 594 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐵 ∧ (𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢)) → (𝑥 ∈ 𝐵 ∧ (𝑢 = {𝑥} ∧ 𝑧 ∈ {𝑥}))) |
23 | 22 | eximi 1899 |
. . . . . . . . . . . 12
⊢
(∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑢 = {𝑥} ∧ 𝑧 ∈ 𝑢)) → ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑢 = {𝑥} ∧ 𝑧 ∈ {𝑥}))) |
24 | 17, 23 | sylbi 207 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑢 ∧ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}) → ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑢 = {𝑥} ∧ 𝑧 ∈ {𝑥}))) |
25 | | an12 873 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐵 ∧ (𝑢 = {𝑥} ∧ 𝑧 ∈ {𝑥})) ↔ (𝑢 = {𝑥} ∧ (𝑥 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}))) |
26 | 25 | exbii 1911 |
. . . . . . . . . . . 12
⊢
(∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑢 = {𝑥} ∧ 𝑧 ∈ {𝑥})) ↔ ∃𝑥(𝑢 = {𝑥} ∧ (𝑥 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}))) |
27 | | exsimpr 1933 |
. . . . . . . . . . . 12
⊢
(∃𝑥(𝑢 = {𝑥} ∧ (𝑥 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) |
28 | 26, 27 | sylbi 207 |
. . . . . . . . . . 11
⊢
(∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑢 = {𝑥} ∧ 𝑧 ∈ {𝑥})) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) |
29 | 24, 28 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑢 ∧ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) |
30 | 29 | exlimiv 1995 |
. . . . . . . . 9
⊢
(∃𝑢(𝑧 ∈ 𝑢 ∧ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) |
31 | 13, 30 | sylbi 207 |
. . . . . . . 8
⊢ (𝑧 ∈ ∪ {𝑢
∣ ∃𝑥 ∈
𝐵 𝑢 = {𝑥}} → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) |
32 | | velsn 4325 |
. . . . . . . . . 10
⊢ (𝑧 ∈ {𝑥} ↔ 𝑧 = 𝑥) |
33 | 32 | anbi2i 732 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ↔ (𝑥 ∈ 𝐵 ∧ 𝑧 = 𝑥)) |
34 | 33 | exbii 1911 |
. . . . . . . 8
⊢
(∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑧 = 𝑥)) |
35 | 31, 34 | sylib 208 |
. . . . . . 7
⊢ (𝑧 ∈ ∪ {𝑢
∣ ∃𝑥 ∈
𝐵 𝑢 = {𝑥}} → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑧 = 𝑥)) |
36 | 12 | biimparc 505 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑧 = 𝑥) → 𝑧 ∈ 𝐵) |
37 | 36 | exlimiv 1995 |
. . . . . . 7
⊢
(∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑧 = 𝑥) → 𝑧 ∈ 𝐵) |
38 | 35, 37 | syl 17 |
. . . . . 6
⊢ (𝑧 ∈ ∪ {𝑢
∣ ∃𝑥 ∈
𝐵 𝑢 = {𝑥}} → 𝑧 ∈ 𝐵) |
39 | 12, 38 | vtoclga 3400 |
. . . . 5
⊢ (𝑥 ∈ ∪ {𝑢
∣ ∃𝑥 ∈
𝐵 𝑢 = {𝑥}} → 𝑥 ∈ 𝐵) |
40 | | equid 2082 |
. . . . . 6
⊢ 𝑥 = 𝑥 |
41 | | eqid 2748 |
. . . . . . . . . . . 12
⊢ {𝑥} = {𝑥} |
42 | | snex 5045 |
. . . . . . . . . . . . . 14
⊢ {𝑥} ∈ V |
43 | | sbcg 3632 |
. . . . . . . . . . . . . 14
⊢ ({𝑥} ∈ V →
([{𝑥} / 𝑢]𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵)) |
44 | 42, 43 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
([{𝑥} / 𝑢]𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵) |
45 | | eqsbc3 3604 |
. . . . . . . . . . . . . 14
⊢ ({𝑥} ∈ V →
([{𝑥} / 𝑢]𝑢 = {𝑥} ↔ {𝑥} = {𝑥})) |
46 | 42, 45 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
([{𝑥} / 𝑢]𝑢 = {𝑥} ↔ {𝑥} = {𝑥}) |
47 | 18 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → (𝑧 ∈ 𝑢 ↔ 𝑧 ∈ {𝑥})) |
48 | | df-rex 3044 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑥 ∈
𝐵 𝑢 = {𝑥} ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥})) |
49 | 13 | biimpri 218 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∃𝑢(𝑧 ∈ 𝑢 ∧ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}) → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) |
50 | 49 | 19.23bi 2196 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ 𝑢 ∧ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}) → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) |
51 | 50 | expcom 450 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑥 ∈
𝐵 𝑢 = {𝑥} → (𝑧 ∈ 𝑢 → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
52 | 48, 51 | sylbir 225 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → (𝑧 ∈ 𝑢 → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
53 | 52 | 19.23bi 2196 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → (𝑧 ∈ 𝑢 → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
54 | 47, 53 | sylbird 250 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → (𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
55 | 54 | sbcth 3579 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑥} ∈ V → [{𝑥} / 𝑢]((𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → (𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}))) |
56 | 42, 55 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
[{𝑥} / 𝑢]((𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → (𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
57 | | sbcimg 3606 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑥} ∈ V →
([{𝑥} / 𝑢]((𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → (𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) ↔ ([{𝑥} / 𝑢](𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → [{𝑥} / 𝑢](𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})))) |
58 | 42, 57 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
([{𝑥} / 𝑢]((𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → (𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) ↔ ([{𝑥} / 𝑢](𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → [{𝑥} / 𝑢](𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}))) |
59 | 56, 58 | mpbi 220 |
. . . . . . . . . . . . . 14
⊢
([{𝑥} / 𝑢](𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) → [{𝑥} / 𝑢](𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
60 | | sbcan 3607 |
. . . . . . . . . . . . . 14
⊢
([{𝑥} / 𝑢](𝑥 ∈ 𝐵 ∧ 𝑢 = {𝑥}) ↔ ([{𝑥} / 𝑢]𝑥 ∈ 𝐵 ∧ [{𝑥} / 𝑢]𝑢 = {𝑥})) |
61 | | nfv 1980 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑢 𝑧 ∈ {𝑥} |
62 | | nfab1 2892 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑢{𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}} |
63 | 62 | nfuni 4582 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑢∪ {𝑢
∣ ∃𝑥 ∈
𝐵 𝑢 = {𝑥}} |
64 | 63 | nfcri 2884 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑢 𝑧 ∈ ∪ {𝑢
∣ ∃𝑥 ∈
𝐵 𝑢 = {𝑥}} |
65 | 61, 64 | nfim 1962 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑢(𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) |
66 | | sbctt 3629 |
. . . . . . . . . . . . . . 15
⊢ (({𝑥} ∈ V ∧ Ⅎ𝑢(𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) → ([{𝑥} / 𝑢](𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) ↔ (𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}))) |
67 | 42, 65, 66 | mp2an 710 |
. . . . . . . . . . . . . 14
⊢
([{𝑥} / 𝑢](𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) ↔ (𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
68 | 59, 60, 67 | 3imtr3i 280 |
. . . . . . . . . . . . 13
⊢
(([{𝑥} /
𝑢]𝑥 ∈ 𝐵 ∧ [{𝑥} / 𝑢]𝑢 = {𝑥}) → (𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
69 | 44, 46, 68 | syl2anbr 498 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐵 ∧ {𝑥} = {𝑥}) → (𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
70 | 41, 69 | mpan2 709 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐵 → (𝑧 ∈ {𝑥} → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
71 | 32, 70 | syl5bir 233 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐵 → (𝑧 = 𝑥 → 𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
72 | | eleq1 2815 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → (𝑧 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}} ↔ 𝑥 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
73 | 71, 72 | mpbidi 231 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → (𝑧 = 𝑥 → 𝑥 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
74 | 73 | com12 32 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
75 | 74 | sbimi 2040 |
. . . . . . 7
⊢ ([𝑥 / 𝑧]𝑧 = 𝑥 → [𝑥 / 𝑧](𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
76 | | equsb3 2557 |
. . . . . . 7
⊢ ([𝑥 / 𝑧]𝑧 = 𝑥 ↔ 𝑥 = 𝑥) |
77 | | nfv 1980 |
. . . . . . . 8
⊢
Ⅎ𝑧(𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) |
78 | 77 | sbf 2505 |
. . . . . . 7
⊢ ([𝑥 / 𝑧](𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) ↔ (𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
79 | 75, 76, 78 | 3imtr3i 280 |
. . . . . 6
⊢ (𝑥 = 𝑥 → (𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})) |
80 | 40, 79 | ax-mp 5 |
. . . . 5
⊢ (𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) |
81 | 39, 80 | impbii 199 |
. . . 4
⊢ (𝑥 ∈ ∪ {𝑢
∣ ∃𝑥 ∈
𝐵 𝑢 = {𝑥}} ↔ 𝑥 ∈ 𝐵) |
82 | 11, 81 | syl6bb 276 |
. . 3
⊢ (𝐵 ⊆ 𝐴 → (𝑥 ∈ ∪ (𝐹 “ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
83 | 82 | eqrdv 2746 |
. 2
⊢ (𝐵 ⊆ 𝐴 → ∪ (𝐹 “ 𝐵) = 𝐵) |
84 | 83 | eqcomd 2754 |
1
⊢ (𝐵 ⊆ 𝐴 → 𝐵 = ∪ (𝐹 “ 𝐵)) |