Theorem dfif5

Description: Alternate definition of the conditional operator df-if . Note that ph is independent of x i.e. a constant true or false (see also ab0orv ). (Contributed by Gérard Lang, 18-Aug-2013)

	Ref	Expression
Hypothesis	dfif3.1	$$⊢C=\left\{x|\phi \right\}$$
Assertion	dfif5	$$⊢if\left(\phi ,A,B\right)=\left(A\cap B\right)\cup \left(\left(\left(A\setminus B\right)\cap C\right)\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfif3.1	$$⊢C=\left\{x|\phi \right\}$$
2		inindi	$$⊢\left(A\cup B\right)\cap \left(\left(A\cup \left(\mathrm{V}\setminus C\right)\right)\cap \left(B\cup C\right)\right)=\left(\left(A\cup B\right)\cap \left(A\cup \left(\mathrm{V}\setminus C\right)\right)\right)\cap \left(\left(A\cup B\right)\cap \left(B\cup C\right)\right)$$
3	1	dfif4	$$⊢if\left(\phi ,A,B\right)=\left(A\cup B\right)\cap \left(\left(A\cup \left(\mathrm{V}\setminus C\right)\right)\cap \left(B\cup C\right)\right)$$
4		undir	$$⊢\left(A\cap B\right)\cup \left(\left(\left(A\setminus B\right)\cap C\right)\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)=\left(A\cup \left(\left(\left(A\setminus B\right)\cap C\right)\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)\right)\cap \left(B\cup \left(\left(\left(A\setminus B\right)\cap C\right)\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)\right)$$
5		unidm	$$⊢A\cup A=A$$
6	5	uneq1i	$$⊢\left(A\cup A\right)\cup \left(B\cap \left(\mathrm{V}\setminus C\right)\right)=A\cup \left(B\cap \left(\mathrm{V}\setminus C\right)\right)$$
7		unass	$$⊢\left(A\cup A\right)\cup \left(B\cap \left(\mathrm{V}\setminus C\right)\right)=A\cup \left(A\cup \left(B\cap \left(\mathrm{V}\setminus C\right)\right)\right)$$
8		undi	$$⊢A\cup \left(B\cap \left(\mathrm{V}\setminus C\right)\right)=\left(A\cup B\right)\cap \left(A\cup \left(\mathrm{V}\setminus C\right)\right)$$
9	6 7 8	3eqtr3ri	$$⊢\left(A\cup B\right)\cap \left(A\cup \left(\mathrm{V}\setminus C\right)\right)=A\cup \left(A\cup \left(B\cap \left(\mathrm{V}\setminus C\right)\right)\right)$$
10		undi	$$⊢A\cup \left(\left(A\setminus B\right)\cap C\right)=\left(A\cup \left(A\setminus B\right)\right)\cap \left(A\cup C\right)$$
11		undifabs	$$⊢A\cup \left(A\setminus B\right)=A$$
12	11	ineq1i	$$⊢\left(A\cup \left(A\setminus B\right)\right)\cap \left(A\cup C\right)=A\cap \left(A\cup C\right)$$
13		inabs	$$⊢A\cap \left(A\cup C\right)=A$$
14	10 12 13	3eqtri	$$⊢A\cup \left(\left(A\setminus B\right)\cap C\right)=A$$
15		undif2	$$⊢A\cup \left(B\setminus A\right)=A\cup B$$
16	15	ineq1i	$$⊢\left(A\cup \left(B\setminus A\right)\right)\cap \left(A\cup \left(\mathrm{V}\setminus C\right)\right)=\left(A\cup B\right)\cap \left(A\cup \left(\mathrm{V}\setminus C\right)\right)$$
17		undi	$$⊢A\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)=\left(A\cup \left(B\setminus A\right)\right)\cap \left(A\cup \left(\mathrm{V}\setminus C\right)\right)$$
18	16 17 8	3eqtr4i	$$⊢A\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)=A\cup \left(B\cap \left(\mathrm{V}\setminus C\right)\right)$$
19	14 18	uneq12i	$$⊢\left(A\cup \left(\left(A\setminus B\right)\cap C\right)\right)\cup \left(A\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)=A\cup \left(A\cup \left(B\cap \left(\mathrm{V}\setminus C\right)\right)\right)$$
20	9 19	eqtr4i	$$⊢\left(A\cup B\right)\cap \left(A\cup \left(\mathrm{V}\setminus C\right)\right)=\left(A\cup \left(\left(A\setminus B\right)\cap C\right)\right)\cup \left(A\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)$$
21		unundi	$$⊢A\cup \left(\left(\left(A\setminus B\right)\cap C\right)\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)=\left(A\cup \left(\left(A\setminus B\right)\cap C\right)\right)\cup \left(A\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)$$
22	20 21	eqtr4i	$$⊢\left(A\cup B\right)\cap \left(A\cup \left(\mathrm{V}\setminus C\right)\right)=A\cup \left(\left(\left(A\setminus B\right)\cap C\right)\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)$$
23		unass	$$⊢\left(\left(A\cap C\right)\cup B\right)\cup B=\left(A\cap C\right)\cup \left(B\cup B\right)$$
24		undi	$$⊢B\cup \left(A\cap C\right)=\left(B\cup A\right)\cap \left(B\cup C\right)$$
25		uncom	$$⊢\left(A\cap C\right)\cup B=B\cup \left(A\cap C\right)$$
26		undif2	$$⊢B\cup \left(A\setminus B\right)=B\cup A$$
27	26	ineq1i	$$⊢\left(B\cup \left(A\setminus B\right)\right)\cap \left(B\cup C\right)=\left(B\cup A\right)\cap \left(B\cup C\right)$$
28	24 25 27	3eqtr4i	$$⊢\left(A\cap C\right)\cup B=\left(B\cup \left(A\setminus B\right)\right)\cap \left(B\cup C\right)$$
29		undi	$$⊢B\cup \left(\left(A\setminus B\right)\cap C\right)=\left(B\cup \left(A\setminus B\right)\right)\cap \left(B\cup C\right)$$
30	28 29	eqtr4i	$$⊢\left(A\cap C\right)\cup B=B\cup \left(\left(A\setminus B\right)\cap C\right)$$
31		undi	$$⊢B\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)=\left(B\cup \left(B\setminus A\right)\right)\cap \left(B\cup \left(\mathrm{V}\setminus C\right)\right)$$
32		undifabs	$$⊢B\cup \left(B\setminus A\right)=B$$
33	32	ineq1i	$$⊢\left(B\cup \left(B\setminus A\right)\right)\cap \left(B\cup \left(\mathrm{V}\setminus C\right)\right)=B\cap \left(B\cup \left(\mathrm{V}\setminus C\right)\right)$$
34		inabs	$$⊢B\cap \left(B\cup \left(\mathrm{V}\setminus C\right)\right)=B$$
35	31 33 34	3eqtrri	$$⊢B=B\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)$$
36	30 35	uneq12i	$$⊢\left(\left(A\cap C\right)\cup B\right)\cup B=\left(B\cup \left(\left(A\setminus B\right)\cap C\right)\right)\cup \left(B\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)$$
37		unidm	$$⊢B\cup B=B$$
38	37	uneq2i	$$⊢\left(A\cap C\right)\cup \left(B\cup B\right)=\left(A\cap C\right)\cup B$$
39	23 36 38	3eqtr3ri	$$⊢\left(A\cap C\right)\cup B=\left(B\cup \left(\left(A\setminus B\right)\cap C\right)\right)\cup \left(B\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)$$
40		uncom	$$⊢B\cup C=C\cup B$$
41	40	ineq2i	$$⊢\left(A\cup B\right)\cap \left(B\cup C\right)=\left(A\cup B\right)\cap \left(C\cup B\right)$$
42		undir	$$⊢\left(A\cap C\right)\cup B=\left(A\cup B\right)\cap \left(C\cup B\right)$$
43	41 42	eqtr4i	$$⊢\left(A\cup B\right)\cap \left(B\cup C\right)=\left(A\cap C\right)\cup B$$
44		unundi	$$⊢B\cup \left(\left(\left(A\setminus B\right)\cap C\right)\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)=\left(B\cup \left(\left(A\setminus B\right)\cap C\right)\right)\cup \left(B\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)$$
45	39 43 44	3eqtr4i	$$⊢\left(A\cup B\right)\cap \left(B\cup C\right)=B\cup \left(\left(\left(A\setminus B\right)\cap C\right)\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)$$
46	22 45	ineq12i	$$⊢\left(\left(A\cup B\right)\cap \left(A\cup \left(\mathrm{V}\setminus C\right)\right)\right)\cap \left(\left(A\cup B\right)\cap \left(B\cup C\right)\right)=\left(A\cup \left(\left(\left(A\setminus B\right)\cap C\right)\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)\right)\cap \left(B\cup \left(\left(\left(A\setminus B\right)\cap C\right)\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)\right)$$
47	4 46	eqtr4i	$$⊢\left(A\cap B\right)\cup \left(\left(\left(A\setminus B\right)\cap C\right)\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)=\left(\left(A\cup B\right)\cap \left(A\cup \left(\mathrm{V}\setminus C\right)\right)\right)\cap \left(\left(A\cup B\right)\cap \left(B\cup C\right)\right)$$
48	2 3 47	3eqtr4i	$$⊢if\left(\phi ,A,B\right)=\left(A\cap B\right)\cup \left(\left(\left(A\setminus B\right)\cap C\right)\cup \left(\left(B\setminus A\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)$$