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