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	$$⊢\left(x\in A⟼if\left(x\in B,C,D\right)\right)=\left(x\in \left(A\cap B\right)⟼C\right)\cup \left(x\in \left(A\setminus B\right)⟼D\right)$$

Proof

Step	Hyp	Ref	Expression
1		mptun	$$⊢\left(x\in \left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)⟼if\left(x\in B,C,D\right)\right)=\left(x\in \left(A\cap B\right)⟼if\left(x\in B,C,D\right)\right)\cup \left(x\in \left(A\setminus B\right)⟼if\left(x\in B,C,D\right)\right)$$
2		inundif	$$⊢\left(A\cap B\right)\cup \left(A\setminus B\right)=A$$
3		eqid	$$⊢if\left(x\in B,C,D\right)=if\left(x\in B,C,D\right)$$
4	2 3	mpteq12i	$$⊢\left(x\in \left(\left(A\cap B\right)\cup \left(A\setminus B\right)\right)⟼if\left(x\in B,C,D\right)\right)=\left(x\in A⟼if\left(x\in B,C,D\right)\right)$$
5		elinel2	$$⊢x\in \left(A\cap B\right)\to x\in B$$
6	5	iftrued	$$⊢x\in \left(A\cap B\right)\to if\left(x\in B,C,D\right)=C$$
7	6	mpteq2ia	$$⊢\left(x\in \left(A\cap B\right)⟼if\left(x\in B,C,D\right)\right)=\left(x\in \left(A\cap B\right)⟼C\right)$$
8		eldifn	$$⊢x\in \left(A\setminus B\right)\to \neg x\in B$$
9	8	iffalsed	$$⊢x\in \left(A\setminus B\right)\to if\left(x\in B,C,D\right)=D$$
10	9	mpteq2ia	$$⊢\left(x\in \left(A\setminus B\right)⟼if\left(x\in B,C,D\right)\right)=\left(x\in \left(A\setminus B\right)⟼D\right)$$
11	7 10	uneq12i	$$⊢\left(x\in \left(A\cap B\right)⟼if\left(x\in B,C,D\right)\right)\cup \left(x\in \left(A\setminus B\right)⟼if\left(x\in B,C,D\right)\right)=\left(x\in \left(A\cap B\right)⟼C\right)\cup \left(x\in \left(A\setminus B\right)⟼D\right)$$
12	1 4 11	3eqtr3i	$$⊢\left(x\in A⟼if\left(x\in B,C,D\right)\right)=\left(x\in \left(A\cap B\right)⟼C\right)\cup \left(x\in \left(A\setminus B\right)⟼D\right)$$