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 } )