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