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

Metamath Proof Explorer

Theorem subval

Description: Value of subtraction, which is the (unique) element x such that B + x = A . (Contributed by NM, 4-Aug-2007) (Revised by Mario Carneiro, 2-Nov-2013)

Ref Expression
Assertion subval 
|- ( ( A e. CC /\ B e. CC ) -> ( A - B ) = ( iota_ x e. CC ( B + x ) = A ) )

Proof

Step Hyp Ref Expression
1 eqeq2 
 |-  ( y = A -> ( ( z + x ) = y <-> ( z + x ) = A ) )
2 1 riotabidv 
 |-  ( y = A -> ( iota_ x e. CC ( z + x ) = y ) = ( iota_ x e. CC ( z + x ) = A ) )
3 oveq1 
 |-  ( z = B -> ( z + x ) = ( B + x ) )
4 3 eqeq1d 
 |-  ( z = B -> ( ( z + x ) = A <-> ( B + x ) = A ) )
5 4 riotabidv 
 |-  ( z = B -> ( iota_ x e. CC ( z + x ) = A ) = ( iota_ x e. CC ( B + x ) = A ) )
6 df-sub 
 |-  - = ( y e. CC , z e. CC |-> ( iota_ x e. CC ( z + x ) = y ) )
7 riotaex 
 |-  ( iota_ x e. CC ( B + x ) = A ) e. _V
8 2 5 6 7 ovmpo 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) = ( iota_ x e. CC ( B + x ) = A ) )