Theorem opabbidv

Description: Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995)

	Ref	Expression
Hypothesis	opabbidv.1	|- ( ph -> ( ps <-> ch ) )
Assertion	opabbidv	|- ( ph -> { <. x , y >. | ps } = { <. x , y >. | ch } )

Proof

Step	Hyp	Ref	Expression
1		opabbidv.1	|- ( ph -> ( ps <-> ch ) )
2		nfv	|- F/ x ph
3		nfv	|- F/ y ph
4	2 3 1	opabbid	|- ( ph -> { <. x , y >. | ps } = { <. x , y >. | ch } )