Description: Deduce equality of a relation and an ordered-pair class abstraction. Compare abbi2dv . (Contributed by NM, 24-Feb-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | opabbi2dv.1 | |- Rel A |
|
opabbi2dv.3 | |- ( ph -> ( <. x , y >. e. A <-> ps ) ) |
||
Assertion | opabbi2dv | |- ( ph -> A = { <. x , y >. | ps } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opabbi2dv.1 | |- Rel A |
|
2 | opabbi2dv.3 | |- ( ph -> ( <. x , y >. e. A <-> ps ) ) |
|
3 | opabid2 | |- ( Rel A -> { <. x , y >. | <. x , y >. e. A } = A ) |
|
4 | 1 3 | ax-mp | |- { <. x , y >. | <. x , y >. e. A } = A |
5 | 2 | opabbidv | |- ( ph -> { <. x , y >. | <. x , y >. e. A } = { <. x , y >. | ps } ) |
6 | 4 5 | syl5eqr | |- ( ph -> A = { <. x , y >. | ps } ) |