| 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 |