Metamath Proof Explorer


Theorem sn-subf

Description: subf without ax-mulcom . (Contributed by SN, 5-May-2024)

Ref Expression
Assertion sn-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 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