Step |
Hyp |
Ref |
Expression |
1 |
|
reuhypd.1 |
|- ( ( ph /\ x e. C ) -> B e. C ) |
2 |
|
reuhypd.2 |
|- ( ( ph /\ x e. C /\ y e. C ) -> ( x = A <-> y = B ) ) |
3 |
1
|
elexd |
|- ( ( ph /\ x e. C ) -> B e. _V ) |
4 |
|
eueq |
|- ( B e. _V <-> E! y y = B ) |
5 |
3 4
|
sylib |
|- ( ( ph /\ x e. C ) -> E! y y = B ) |
6 |
|
eleq1 |
|- ( y = B -> ( y e. C <-> B e. C ) ) |
7 |
1 6
|
syl5ibrcom |
|- ( ( ph /\ x e. C ) -> ( y = B -> y e. C ) ) |
8 |
7
|
pm4.71rd |
|- ( ( ph /\ x e. C ) -> ( y = B <-> ( y e. C /\ y = B ) ) ) |
9 |
2
|
3expa |
|- ( ( ( ph /\ x e. C ) /\ y e. C ) -> ( x = A <-> y = B ) ) |
10 |
9
|
pm5.32da |
|- ( ( ph /\ x e. C ) -> ( ( y e. C /\ x = A ) <-> ( y e. C /\ y = B ) ) ) |
11 |
8 10
|
bitr4d |
|- ( ( ph /\ x e. C ) -> ( y = B <-> ( y e. C /\ x = A ) ) ) |
12 |
11
|
eubidv |
|- ( ( ph /\ x e. C ) -> ( E! y y = B <-> E! y ( y e. C /\ x = A ) ) ) |
13 |
5 12
|
mpbid |
|- ( ( ph /\ x e. C ) -> E! y ( y e. C /\ x = A ) ) |
14 |
|
df-reu |
|- ( E! y e. C x = A <-> E! y ( y e. C /\ x = A ) ) |
15 |
13 14
|
sylibr |
|- ( ( ph /\ x e. C ) -> E! y e. C x = A ) |