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