Theorem oprabbidv

Description: Equivalent wff's yield equal operation class abstractions (deduction form). (Contributed by NM, 21-Feb-2004)

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

Proof

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