Step |
Hyp |
Ref |
Expression |
1 |
|
opabbid.1 |
|- F/ x ph |
2 |
|
opabbid.2 |
|- F/ y ph |
3 |
|
opabbid.3 |
|- ( ph -> ( ps <-> ch ) ) |
4 |
3
|
anbi2d |
|- ( ph -> ( ( z = <. x , y >. /\ ps ) <-> ( z = <. x , y >. /\ ch ) ) ) |
5 |
2 4
|
exbid |
|- ( ph -> ( E. y ( z = <. x , y >. /\ ps ) <-> E. y ( z = <. x , y >. /\ ch ) ) ) |
6 |
1 5
|
exbid |
|- ( ph -> ( E. x E. y ( z = <. x , y >. /\ ps ) <-> E. x E. y ( z = <. x , y >. /\ ch ) ) ) |
7 |
6
|
abbidv |
|- ( ph -> { z | E. x E. y ( z = <. x , y >. /\ ps ) } = { z | E. x E. y ( z = <. x , y >. /\ ch ) } ) |
8 |
|
df-opab |
|- { <. x , y >. | ps } = { z | E. x E. y ( z = <. x , y >. /\ ps ) } |
9 |
|
df-opab |
|- { <. x , y >. | ch } = { z | E. x E. y ( z = <. x , y >. /\ ch ) } |
10 |
7 8 9
|
3eqtr4g |
|- ( ph -> { <. x , y >. | ps } = { <. x , y >. | ch } ) |