Step |
Hyp |
Ref |
Expression |
1 |
|
df-iota |
⊢ ( ℩ 𝑥 𝜑 ) = ∪ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } |
2 |
|
abeq1 |
⊢ ( { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = ∪ { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) } ↔ ∀ 𝑦 ( { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ 𝑦 ∈ ∪ { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) } ) ) |
3 |
|
exdistr |
⊢ ( ∃ 𝑧 ∃ 𝑤 ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) ↔ ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) ) |
4 |
|
vex |
⊢ 𝑦 ∈ V |
5 |
|
sneq |
⊢ ( 𝑤 = 𝑦 → { 𝑤 } = { 𝑦 } ) |
6 |
5
|
eqeq2d |
⊢ ( 𝑤 = 𝑦 → ( { 𝑥 ∣ 𝜑 } = { 𝑤 } ↔ { 𝑥 ∣ 𝜑 } = { 𝑦 } ) ) |
7 |
4 6
|
ceqsexv |
⊢ ( ∃ 𝑤 ( 𝑤 = 𝑦 ∧ { 𝑥 ∣ 𝜑 } = { 𝑤 } ) ↔ { 𝑥 ∣ 𝜑 } = { 𝑦 } ) |
8 |
|
snex |
⊢ { 𝑤 } ∈ V |
9 |
|
eqeq1 |
⊢ ( 𝑧 = { 𝑤 } → ( 𝑧 = { 𝑥 ∣ 𝜑 } ↔ { 𝑤 } = { 𝑥 ∣ 𝜑 } ) ) |
10 |
|
eleq2 |
⊢ ( 𝑧 = { 𝑤 } → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ { 𝑤 } ) ) |
11 |
9 10
|
anbi12d |
⊢ ( 𝑧 = { 𝑤 } → ( ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑦 ∈ 𝑧 ) ↔ ( { 𝑤 } = { 𝑥 ∣ 𝜑 } ∧ 𝑦 ∈ { 𝑤 } ) ) ) |
12 |
|
eqcom |
⊢ ( { 𝑤 } = { 𝑥 ∣ 𝜑 } ↔ { 𝑥 ∣ 𝜑 } = { 𝑤 } ) |
13 |
|
velsn |
⊢ ( 𝑦 ∈ { 𝑤 } ↔ 𝑦 = 𝑤 ) |
14 |
|
equcom |
⊢ ( 𝑦 = 𝑤 ↔ 𝑤 = 𝑦 ) |
15 |
13 14
|
bitri |
⊢ ( 𝑦 ∈ { 𝑤 } ↔ 𝑤 = 𝑦 ) |
16 |
12 15
|
anbi12ci |
⊢ ( ( { 𝑤 } = { 𝑥 ∣ 𝜑 } ∧ 𝑦 ∈ { 𝑤 } ) ↔ ( 𝑤 = 𝑦 ∧ { 𝑥 ∣ 𝜑 } = { 𝑤 } ) ) |
17 |
11 16
|
bitrdi |
⊢ ( 𝑧 = { 𝑤 } → ( ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑦 ∈ 𝑧 ) ↔ ( 𝑤 = 𝑦 ∧ { 𝑥 ∣ 𝜑 } = { 𝑤 } ) ) ) |
18 |
8 17
|
ceqsexv |
⊢ ( ∃ 𝑧 ( 𝑧 = { 𝑤 } ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑦 ∈ 𝑧 ) ) ↔ ( 𝑤 = 𝑦 ∧ { 𝑥 ∣ 𝜑 } = { 𝑤 } ) ) |
19 |
|
an13 |
⊢ ( ( 𝑧 = { 𝑤 } ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑦 ∈ 𝑧 ) ) ↔ ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) ) |
20 |
19
|
exbii |
⊢ ( ∃ 𝑧 ( 𝑧 = { 𝑤 } ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑦 ∈ 𝑧 ) ) ↔ ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) ) |
21 |
18 20
|
bitr3i |
⊢ ( ( 𝑤 = 𝑦 ∧ { 𝑥 ∣ 𝜑 } = { 𝑤 } ) ↔ ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) ) |
22 |
21
|
exbii |
⊢ ( ∃ 𝑤 ( 𝑤 = 𝑦 ∧ { 𝑥 ∣ 𝜑 } = { 𝑤 } ) ↔ ∃ 𝑤 ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) ) |
23 |
7 22
|
bitr3i |
⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ ∃ 𝑤 ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) ) |
24 |
|
excom |
⊢ ( ∃ 𝑤 ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) ) |
25 |
23 24
|
bitri |
⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) ) |
26 |
|
eluniab |
⊢ ( 𝑦 ∈ ∪ { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) } ↔ ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) ) |
27 |
3 25 26
|
3bitr4i |
⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ 𝑦 ∈ ∪ { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) } ) |
28 |
2 27
|
mpgbir |
⊢ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = ∪ { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) } |
29 |
|
df-sn |
⊢ { { 𝑥 ∣ 𝜑 } } = { 𝑧 ∣ 𝑧 = { 𝑥 ∣ 𝜑 } } |
30 |
|
dfsingles2 |
⊢ Singletons = { 𝑧 ∣ ∃ 𝑤 𝑧 = { 𝑤 } } |
31 |
29 30
|
ineq12i |
⊢ ( { { 𝑥 ∣ 𝜑 } } ∩ Singletons ) = ( { 𝑧 ∣ 𝑧 = { 𝑥 ∣ 𝜑 } } ∩ { 𝑧 ∣ ∃ 𝑤 𝑧 = { 𝑤 } } ) |
32 |
|
inab |
⊢ ( { 𝑧 ∣ 𝑧 = { 𝑥 ∣ 𝜑 } } ∩ { 𝑧 ∣ ∃ 𝑤 𝑧 = { 𝑤 } } ) = { 𝑧 ∣ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ ∃ 𝑤 𝑧 = { 𝑤 } ) } |
33 |
|
19.42v |
⊢ ( ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ↔ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ ∃ 𝑤 𝑧 = { 𝑤 } ) ) |
34 |
33
|
bicomi |
⊢ ( ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ ∃ 𝑤 𝑧 = { 𝑤 } ) ↔ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) |
35 |
34
|
abbii |
⊢ { 𝑧 ∣ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ ∃ 𝑤 𝑧 = { 𝑤 } ) } = { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) } |
36 |
32 35
|
eqtri |
⊢ ( { 𝑧 ∣ 𝑧 = { 𝑥 ∣ 𝜑 } } ∩ { 𝑧 ∣ ∃ 𝑤 𝑧 = { 𝑤 } } ) = { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) } |
37 |
31 36
|
eqtri |
⊢ ( { { 𝑥 ∣ 𝜑 } } ∩ Singletons ) = { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) } |
38 |
37
|
unieqi |
⊢ ∪ ( { { 𝑥 ∣ 𝜑 } } ∩ Singletons ) = ∪ { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) } |
39 |
28 38
|
eqtr4i |
⊢ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = ∪ ( { { 𝑥 ∣ 𝜑 } } ∩ Singletons ) |
40 |
39
|
unieqi |
⊢ ∪ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = ∪ ∪ ( { { 𝑥 ∣ 𝜑 } } ∩ Singletons ) |
41 |
1 40
|
eqtri |
⊢ ( ℩ 𝑥 𝜑 ) = ∪ ∪ ( { { 𝑥 ∣ 𝜑 } } ∩ Singletons ) |