Theorem partfun

Description: Rewrite a function defined by parts, using a mapping and an if construct, into a union of functions on disjoint domains. (Contributed by Thierry Arnoux, 30-Mar-2017)

	Ref	Expression
Assertion	partfun	|- ( x e. A |-> if ( x e. B , C , D ) ) = ( ( x e. ( A i^i B ) |-> C ) u. ( x e. ( A \ B ) |-> D ) )

Proof

Step	Hyp	Ref	Expression
1		mptun	|- ( x e. ( ( A i^i B ) u. ( A \ B ) ) |-> if ( x e. B , C , D ) ) = ( ( x e. ( A i^i B ) |-> if ( x e. B , C , D ) ) u. ( x e. ( A \ B ) |-> if ( x e. B , C , D ) ) )
2		inundif	|- ( ( A i^i B ) u. ( A \ B ) ) = A
3		eqid	|- if ( x e. B , C , D ) = if ( x e. B , C , D )
4	2 3	mpteq12i	|- ( x e. ( ( A i^i B ) u. ( A \ B ) ) |-> if ( x e. B , C , D ) ) = ( x e. A |-> if ( x e. B , C , D ) )
5		elinel2	|- ( x e. ( A i^i B ) -> x e. B )
6	5	iftrued	|- ( x e. ( A i^i B ) -> if ( x e. B , C , D ) = C )
7	6	mpteq2ia	|- ( x e. ( A i^i B ) |-> if ( x e. B , C , D ) ) = ( x e. ( A i^i B ) |-> C )
8		eldifn	|- ( x e. ( A \ B ) -> -. x e. B )
9	8	iffalsed	|- ( x e. ( A \ B ) -> if ( x e. B , C , D ) = D )
10	9	mpteq2ia	|- ( x e. ( A \ B ) |-> if ( x e. B , C , D ) ) = ( x e. ( A \ B ) |-> D )
11	7 10	uneq12i	|- ( ( x e. ( A i^i B ) |-> if ( x e. B , C , D ) ) u. ( x e. ( A \ B ) |-> if ( x e. B , C , D ) ) ) = ( ( x e. ( A i^i B ) |-> C ) u. ( x e. ( A \ B ) |-> D ) )
12	1 4 11	3eqtr3i	|- ( x e. A |-> if ( x e. B , C , D ) ) = ( ( x e. ( A i^i B ) |-> C ) u. ( x e. ( A \ B ) |-> D ) )