Theorem oprabbii

Description: Equivalent wff's yield equal operation class abstractions. (Contributed by NM, 28-May-1995) (Revised by David Abernethy, 19-Jun-2012)

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

Proof

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