Step |
Hyp |
Ref |
Expression |
1 |
|
ralxfrd.1 |
|- ( ( ph /\ y e. C ) -> A e. B ) |
2 |
|
ralxfrd.2 |
|- ( ( ph /\ x e. B ) -> E. y e. C x = A ) |
3 |
|
ralxfrd.3 |
|- ( ( ph /\ x = A ) -> ( ps <-> ch ) ) |
4 |
3
|
adantlr |
|- ( ( ( ph /\ y e. C ) /\ x = A ) -> ( ps <-> ch ) ) |
5 |
1 4
|
rspcdv |
|- ( ( ph /\ y e. C ) -> ( A. x e. B ps -> ch ) ) |
6 |
5
|
ralrimdva |
|- ( ph -> ( A. x e. B ps -> A. y e. C ch ) ) |
7 |
|
r19.29 |
|- ( ( A. y e. C ch /\ E. y e. C x = A ) -> E. y e. C ( ch /\ x = A ) ) |
8 |
3
|
exbiri |
|- ( ph -> ( x = A -> ( ch -> ps ) ) ) |
9 |
8
|
impcomd |
|- ( ph -> ( ( ch /\ x = A ) -> ps ) ) |
10 |
9
|
rexlimdvw |
|- ( ph -> ( E. y e. C ( ch /\ x = A ) -> ps ) ) |
11 |
7 10
|
syl5 |
|- ( ph -> ( ( A. y e. C ch /\ E. y e. C x = A ) -> ps ) ) |
12 |
11
|
adantr |
|- ( ( ph /\ x e. B ) -> ( ( A. y e. C ch /\ E. y e. C x = A ) -> ps ) ) |
13 |
2 12
|
mpan2d |
|- ( ( ph /\ x e. B ) -> ( A. y e. C ch -> ps ) ) |
14 |
13
|
ralrimdva |
|- ( ph -> ( A. y e. C ch -> A. x e. B ps ) ) |
15 |
6 14
|
impbid |
|- ( ph -> ( A. x e. B ps <-> A. y e. C ch ) ) |