This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subf

Description: Subtraction is an operation on the complex numbers. (Contributed by NM, 4-Aug-2007) (Revised by Mario Carneiro, 16-Nov-2013)

Ref Expression
Assertion subf 
|- - : ( CC X. CC ) --> CC

Proof

Step Hyp Ref Expression
1 subval 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x - y ) = ( iota_ z e. CC ( y + z ) = x ) )
2 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