| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-iota |
⊢ ( ℩ 𝑥 𝜑 ) = ∪ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } |
| 2 |
|
eqabcb |
⊢ ( { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = ∪ { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) } ↔ ∀ 𝑦 ( { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ 𝑦 ∈ ∪ { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) } ) ) |
| 3 |
|
exdistr |
⊢ ( ∃ 𝑧 ∃ 𝑤 ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) ↔ ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) ) |
| 4 |
|
vex |
⊢ 𝑦 ∈ V |
| 5 |
|
sneq |
⊢ ( 𝑤 = 𝑦 → { 𝑤 } = { 𝑦 } ) |
| 6 |
5
|
eqeq2d |
⊢ ( 𝑤 = 𝑦 → ( { 𝑥 ∣ 𝜑 } = { 𝑤 } ↔ { 𝑥 ∣ 𝜑 } = { 𝑦 } ) ) |
| 7 |
4 6
|
ceqsexv |
⊢ ( ∃ 𝑤 ( 𝑤 = 𝑦 ∧ { 𝑥 ∣ 𝜑 } = { 𝑤 } ) ↔ { 𝑥 ∣ 𝜑 } = { 𝑦 } ) |
| 8 |
|
vsnex |
⊢ { 𝑤 } ∈ 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 ) |