Step |
Hyp |
Ref |
Expression |
1 |
|
eusvobj1.1 |
|- B e. _V |
2 |
|
euabsn2 |
|- ( E! x E. y e. A x = B <-> E. z { x | E. y e. A x = B } = { z } ) |
3 |
|
eleq2 |
|- ( { x | E. y e. A x = B } = { z } -> ( x e. { x | E. y e. A x = B } <-> x e. { z } ) ) |
4 |
|
abid |
|- ( x e. { x | E. y e. A x = B } <-> E. y e. A x = B ) |
5 |
|
velsn |
|- ( x e. { z } <-> x = z ) |
6 |
3 4 5
|
3bitr3g |
|- ( { x | E. y e. A x = B } = { z } -> ( E. y e. A x = B <-> x = z ) ) |
7 |
|
nfre1 |
|- F/ y E. y e. A x = B |
8 |
7
|
nfab |
|- F/_ y { x | E. y e. A x = B } |
9 |
8
|
nfeq1 |
|- F/ y { x | E. y e. A x = B } = { z } |
10 |
1
|
elabrex |
|- ( y e. A -> B e. { x | E. y e. A x = B } ) |
11 |
|
eleq2 |
|- ( { x | E. y e. A x = B } = { z } -> ( B e. { x | E. y e. A x = B } <-> B e. { z } ) ) |
12 |
1
|
elsn |
|- ( B e. { z } <-> B = z ) |
13 |
|
eqcom |
|- ( B = z <-> z = B ) |
14 |
12 13
|
bitri |
|- ( B e. { z } <-> z = B ) |
15 |
11 14
|
bitrdi |
|- ( { x | E. y e. A x = B } = { z } -> ( B e. { x | E. y e. A x = B } <-> z = B ) ) |
16 |
10 15
|
syl5ib |
|- ( { x | E. y e. A x = B } = { z } -> ( y e. A -> z = B ) ) |
17 |
9 16
|
ralrimi |
|- ( { x | E. y e. A x = B } = { z } -> A. y e. A z = B ) |
18 |
|
eqeq1 |
|- ( x = z -> ( x = B <-> z = B ) ) |
19 |
18
|
ralbidv |
|- ( x = z -> ( A. y e. A x = B <-> A. y e. A z = B ) ) |
20 |
17 19
|
syl5ibrcom |
|- ( { x | E. y e. A x = B } = { z } -> ( x = z -> A. y e. A x = B ) ) |
21 |
6 20
|
sylbid |
|- ( { x | E. y e. A x = B } = { z } -> ( E. y e. A x = B -> A. y e. A x = B ) ) |
22 |
21
|
exlimiv |
|- ( E. z { x | E. y e. A x = B } = { z } -> ( E. y e. A x = B -> A. y e. A x = B ) ) |
23 |
2 22
|
sylbi |
|- ( E! x E. y e. A x = B -> ( E. y e. A x = B -> A. y e. A x = B ) ) |
24 |
|
euex |
|- ( E! x E. y e. A x = B -> E. x E. y e. A x = B ) |
25 |
|
rexn0 |
|- ( E. y e. A x = B -> A =/= (/) ) |
26 |
25
|
exlimiv |
|- ( E. x E. y e. A x = B -> A =/= (/) ) |
27 |
|
r19.2z |
|- ( ( A =/= (/) /\ A. y e. A x = B ) -> E. y e. A x = B ) |
28 |
27
|
ex |
|- ( A =/= (/) -> ( A. y e. A x = B -> E. y e. A x = B ) ) |
29 |
24 26 28
|
3syl |
|- ( E! x E. y e. A x = B -> ( A. y e. A x = B -> E. y e. A x = B ) ) |
30 |
23 29
|
impbid |
|- ( E! x E. y e. A x = B -> ( E. y e. A x = B <-> A. y e. A x = B ) ) |