This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 1 anbi2d 
 |-  ( ph -> ( ( w = <. <. x , y >. , z >. /\ ps ) <-> ( w = <. <. x , y >. , z >. /\ ch ) ) )
3 2 exbidv 
 |-  ( ph -> ( E. z ( w = <. <. x , y >. , z >. /\ ps ) <-> E. z ( w = <. <. x , y >. , z >. /\ ch ) ) )
4 3 exbidv 
 |-  ( ph -> ( E. y E. z ( w = <. <. x , y >. , z >. /\ ps ) <-> E. y E. z ( w = <. <. x , y >. , z >. /\ ch ) ) )
5 4 exbidv 
 |-  ( ph -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ps ) <-> E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ch ) ) )
6 5 abbidv 
 |-  ( ph -> { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ps ) } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ch ) } )
7 df-oprab 
 |-  { <. <. x , y >. , z >. | ps } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ps ) }
8 df-oprab 
 |-  { <. <. x , y >. , z >. | ch } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ch ) }
9 6 7 8 3eqtr4g 
 |-  ( ph -> { <. <. x , y >. , z >. | ps } = { <. <. x , y >. , z >. | ch } )