| Step |
Hyp |
Ref |
Expression |
| 1 |
|
elequ2 |
|- ( x = y -> ( z e. x <-> z e. y ) ) |
| 2 |
1
|
anbi1d |
|- ( x = y -> ( ( z e. x /\ ch ) <-> ( z e. y /\ ch ) ) ) |
| 3 |
2
|
exbidv |
|- ( x = y -> ( E. w ( z e. x /\ ch ) <-> E. w ( z e. y /\ ch ) ) ) |
| 4 |
3
|
bibi2d |
|- ( x = y -> ( ( ps <-> E. w ( z e. x /\ ch ) ) <-> ( ps <-> E. w ( z e. y /\ ch ) ) ) ) |
| 5 |
4
|
albidv |
|- ( x = y -> ( A. v ( ps <-> E. w ( z e. x /\ ch ) ) <-> A. v ( ps <-> E. w ( z e. y /\ ch ) ) ) ) |
| 6 |
5
|
imbi2d |
|- ( x = y -> ( ( ph -> A. v ( ps <-> E. w ( z e. x /\ ch ) ) ) <-> ( ph -> A. v ( ps <-> E. w ( z e. y /\ ch ) ) ) ) ) |
| 7 |
6
|
exbidv |
|- ( x = y -> ( E. u ( ph -> A. v ( ps <-> E. w ( z e. x /\ ch ) ) ) <-> E. u ( ph -> A. v ( ps <-> E. w ( z e. y /\ ch ) ) ) ) ) |