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

Metamath Proof Explorer

Theorem oprabbid

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

Ref Expression
Hypotheses oprabbid.1 
|- F/ x ph
oprabbid.2 
|- F/ y ph
oprabbid.3 
|- F/ z ph
oprabbid.4 
|- ( ph -> ( ps <-> ch ) )
Assertion oprabbid 
|- ( ph -> { <. <. x , y >. , z >. | ps } = { <. <. x , y >. , z >. | ch } )

Proof

Step Hyp Ref Expression
1 oprabbid.1 
 |-  F/ x ph
2 oprabbid.2 
 |-  F/ y ph
3 oprabbid.3 
 |-  F/ z ph
4 oprabbid.4 
 |-  ( ph -> ( ps <-> ch ) )
5 4 anbi2d 
 |-  ( ph -> ( ( w = <. <. x , y >. , z >. /\ ps ) <-> ( w = <. <. x , y >. , z >. /\ ch ) ) )
6 3 5 exbid 
 |-  ( ph -> ( E. z ( w = <. <. x , y >. , z >. /\ ps ) <-> E. z ( w = <. <. x , y >. , z >. /\ ch ) ) )
7 2 6 exbid 
 |-  ( ph -> ( E. y E. z ( w = <. <. x , y >. , z >. /\ ps ) <-> E. y E. z ( w = <. <. x , y >. , z >. /\ ch ) ) )
8 1 7 exbid 
 |-  ( ph -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ps ) <-> E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ch ) ) )
9 8 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 ) } )
10 df-oprab 
 |-  { <. <. x , y >. , z >. | ps } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ps ) }
11 df-oprab 
 |-  { <. <. x , y >. , z >. | ch } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ch ) }
12 9 10 11 3eqtr4g 
 |-  ( ph -> { <. <. x , y >. , z >. | ps } = { <. <. x , y >. , z >. | ch } )