Step |
Hyp |
Ref |
Expression |
1 |
|
subval |
|- ( ( x e. CC /\ y e. CC ) -> ( x - y ) = ( iota_ z e. CC ( y + z ) = x ) ) |
2 |
|
sn-subcl |
|- ( ( x e. CC /\ y e. CC ) -> ( x - y ) e. CC ) |
3 |
1 2
|
eqeltrrd |
|- ( ( x e. CC /\ y e. CC ) -> ( iota_ z e. CC ( y + z ) = x ) e. CC ) |
4 |
3
|
rgen2 |
|- A. x e. CC A. y e. CC ( iota_ z e. CC ( y + z ) = x ) e. CC |
5 |
|
df-sub |
|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) ) |
6 |
5
|
fmpo |
|- ( A. x e. CC A. y e. CC ( iota_ z e. CC ( y + z ) = x ) e. CC <-> - : ( CC X. CC ) --> CC ) |
7 |
4 6
|
mpbi |
|- - : ( CC X. CC ) --> CC |