Step |
Hyp |
Ref |
Expression |
1 |
|
ralxfrd2.1 |
|- ( ( ph /\ y e. C ) -> A e. B ) |
2 |
|
ralxfrd2.2 |
|- ( ( ph /\ x e. B ) -> E. y e. C x = A ) |
3 |
|
ralxfrd2.3 |
|- ( ( ph /\ y e. C /\ x = A ) -> ( ps <-> ch ) ) |
4 |
3
|
notbid |
|- ( ( ph /\ y e. C /\ x = A ) -> ( -. ps <-> -. ch ) ) |
5 |
1 2 4
|
ralxfrd2 |
|- ( ph -> ( A. x e. B -. ps <-> A. y e. C -. ch ) ) |
6 |
5
|
notbid |
|- ( ph -> ( -. A. x e. B -. ps <-> -. A. y e. C -. ch ) ) |
7 |
|
dfrex2 |
|- ( E. x e. B ps <-> -. A. x e. B -. ps ) |
8 |
|
dfrex2 |
|- ( E. y e. C ch <-> -. A. y e. C -. ch ) |
9 |
6 7 8
|
3bitr4g |
|- ( ph -> ( E. x e. B ps <-> E. y e. C ch ) ) |