Theorem opabbii

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

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

Proof

Step	Hyp	Ref	Expression
1		opabbii.1	|- ( ph <-> ps )
2		eqid	|- z = z
3	1	a1i	|- ( z = z -> ( ph <-> ps ) )
4	3	opabbidv	|- ( z = z -> { <. x , y >. | ph } = { <. x , y >. | ps } )
5	2 4	ax-mp	|- { <. x , y >. | ph } = { <. x , y >. | ps }