Step |
Hyp |
Ref |
Expression |
1 |
|
elabreximd.1 |
|- F/ x ph |
2 |
|
elabreximd.2 |
|- F/ x ch |
3 |
|
elabreximd.3 |
|- ( A = B -> ( ch <-> ps ) ) |
4 |
|
elabreximd.4 |
|- ( ph -> A e. V ) |
5 |
|
elabreximd.5 |
|- ( ( ph /\ x e. C ) -> ps ) |
6 |
|
eqeq1 |
|- ( y = A -> ( y = B <-> A = B ) ) |
7 |
6
|
rexbidv |
|- ( y = A -> ( E. x e. C y = B <-> E. x e. C A = B ) ) |
8 |
7
|
elabg |
|- ( A e. V -> ( A e. { y | E. x e. C y = B } <-> E. x e. C A = B ) ) |
9 |
4 8
|
syl |
|- ( ph -> ( A e. { y | E. x e. C y = B } <-> E. x e. C A = B ) ) |
10 |
9
|
biimpa |
|- ( ( ph /\ A e. { y | E. x e. C y = B } ) -> E. x e. C A = B ) |
11 |
|
simpr |
|- ( ( ( ph /\ x e. C ) /\ A = B ) -> A = B ) |
12 |
5
|
adantr |
|- ( ( ( ph /\ x e. C ) /\ A = B ) -> ps ) |
13 |
3
|
biimpar |
|- ( ( A = B /\ ps ) -> ch ) |
14 |
11 12 13
|
syl2anc |
|- ( ( ( ph /\ x e. C ) /\ A = B ) -> ch ) |
15 |
14
|
exp31 |
|- ( ph -> ( x e. C -> ( A = B -> ch ) ) ) |
16 |
1 2 15
|
rexlimd |
|- ( ph -> ( E. x e. C A = B -> ch ) ) |
17 |
16
|
imp |
|- ( ( ph /\ E. x e. C A = B ) -> ch ) |
18 |
10 17
|
syldan |
|- ( ( ph /\ A e. { y | E. x e. C y = B } ) -> ch ) |