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 } ) |