Step |
Hyp |
Ref |
Expression |
1 |
|
dffv3 |
⊢ ( 𝐹 ‘ 𝐴 ) = ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ) |
2 |
|
dfiota3 |
⊢ ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ) = ∪ ∪ ( { { 𝑥 ∣ 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) } } ∩ Singletons ) |
3 |
|
abid2 |
⊢ { 𝑥 ∣ 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) } = ( 𝐹 “ { 𝐴 } ) |
4 |
3
|
sneqi |
⊢ { { 𝑥 ∣ 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) } } = { ( 𝐹 “ { 𝐴 } ) } |
5 |
4
|
ineq1i |
⊢ ( { { 𝑥 ∣ 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) } } ∩ Singletons ) = ( { ( 𝐹 “ { 𝐴 } ) } ∩ Singletons ) |
6 |
5
|
unieqi |
⊢ ∪ ( { { 𝑥 ∣ 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) } } ∩ Singletons ) = ∪ ( { ( 𝐹 “ { 𝐴 } ) } ∩ Singletons ) |
7 |
6
|
unieqi |
⊢ ∪ ∪ ( { { 𝑥 ∣ 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) } } ∩ Singletons ) = ∪ ∪ ( { ( 𝐹 “ { 𝐴 } ) } ∩ Singletons ) |
8 |
1 2 7
|
3eqtri |
⊢ ( 𝐹 ‘ 𝐴 ) = ∪ ∪ ( { ( 𝐹 “ { 𝐴 } ) } ∩ Singletons ) |