Metamath Proof Explorer


Theorem opabbi2dv

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

Proof

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 eqtr3id
 |-  ( ph -> A = { <. x , y >. | ps } )