Step |
Hyp |
Ref |
Expression |
1 |
|
df-reu |
|- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) ) |
2 |
|
sniota |
|- ( E! x ( x e. A /\ ph ) -> { x | ( x e. A /\ ph ) } = { ( iota x ( x e. A /\ ph ) ) } ) |
3 |
1 2
|
sylbi |
|- ( E! x e. A ph -> { x | ( x e. A /\ ph ) } = { ( iota x ( x e. A /\ ph ) ) } ) |
4 |
|
df-rab |
|- { x e. A | ph } = { x | ( x e. A /\ ph ) } |
5 |
|
df-riota |
|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) ) |
6 |
5
|
sneqi |
|- { ( iota_ x e. A ph ) } = { ( iota x ( x e. A /\ ph ) ) } |
7 |
3 4 6
|
3eqtr4g |
|- ( E! x e. A ph -> { x e. A | ph } = { ( iota_ x e. A ph ) } ) |