| Step |
Hyp |
Ref |
Expression |
| 1 |
|
pm4.71 |
|- ( ( x e. A -> ph ) <-> ( x e. A <-> ( x e. A /\ ph ) ) ) |
| 2 |
1
|
albii |
|- ( A. x ( x e. A -> ph ) <-> A. x ( x e. A <-> ( x e. A /\ ph ) ) ) |
| 3 |
|
eqab |
|- ( A. x ( x e. A <-> ( x e. A /\ ph ) ) -> A = { x | ( x e. A /\ ph ) } ) |
| 4 |
2 3
|
sylbi |
|- ( A. x ( x e. A -> ph ) -> A = { x | ( x e. A /\ ph ) } ) |
| 5 |
|
df-ral |
|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) ) |
| 6 |
|
df-rab |
|- { x e. A | ph } = { x | ( x e. A /\ ph ) } |
| 7 |
6
|
eqeq2i |
|- ( A = { x e. A | ph } <-> A = { x | ( x e. A /\ ph ) } ) |
| 8 |
4 5 7
|
3imtr4i |
|- ( A. x e. A ph -> A = { x e. A | ph } ) |