Theorem dfif5 4475

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

Hypothesis

Ref	Expression
dfif3.1	⊢ 𝐶 = {𝑥 ∣ 𝜑}

Assertion

Ref	Expression
dfif5	⊢ if(𝜑, 𝐴, 𝐵) = ((𝐴 ∩ 𝐵) ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem dfif5

Step	Hyp	Ref	Expression
1		inindi 4160	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((𝐴 ∪ (V ∖ 𝐶)) ∩ (𝐵 ∪ 𝐶))) = (((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) ∩ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)))
2		dfif3.1	. . 3 ⊢ 𝐶 = {𝑥 ∣ 𝜑}
3	2	dfif4 4474	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((𝐴 ∪ (V ∖ 𝐶)) ∩ (𝐵 ∪ 𝐶)))
4		undir 4210	. . 3 ⊢ ((𝐴 ∩ 𝐵) ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = ((𝐴 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) ∩ (𝐵 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))))
5		unidm 4086	. . . . . . . 8 ⊢ (𝐴 ∪ 𝐴) = 𝐴
6	5	uneq1i 4093	. . . . . . 7 ⊢ ((𝐴 ∪ 𝐴) ∪ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶)))
7		unass 4100	. . . . . . 7 ⊢ ((𝐴 ∪ 𝐴) ∪ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∪ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))))
8		undi 4208	. . . . . . 7 ⊢ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶)))
9	6, 7, 8	3eqtr3ri 2775	. . . . . 6 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) = (𝐴 ∪ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))))
10		undi 4208	. . . . . . . 8 ⊢ (𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) = ((𝐴 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐴 ∪ 𝐶))
11		undifabs 4411	. . . . . . . . 9 ⊢ (𝐴 ∪ (𝐴 ∖ 𝐵)) = 𝐴
12	11	ineq1i 4142	. . . . . . . 8 ⊢ ((𝐴 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐴 ∪ 𝐶)) = (𝐴 ∩ (𝐴 ∪ 𝐶))
13		inabs 4189	. . . . . . . 8 ⊢ (𝐴 ∩ (𝐴 ∪ 𝐶)) = 𝐴
14	10, 12, 13	3eqtri 2770	. . . . . . 7 ⊢ (𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) = 𝐴
15		undif2 4410	. . . . . . . . 9 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
16	15	ineq1i 4142	. . . . . . . 8 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) ∩ (𝐴 ∪ (V ∖ 𝐶))) = ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶)))
17		undi 4208	. . . . . . . 8 ⊢ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))) = ((𝐴 ∪ (𝐵 ∖ 𝐴)) ∩ (𝐴 ∪ (V ∖ 𝐶)))
18	16, 17, 8	3eqtr4i 2776	. . . . . . 7 ⊢ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))) = (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶)))
19	14, 18	uneq12i 4095	. . . . . 6 ⊢ ((𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = (𝐴 ∪ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))))
20	9, 19	eqtr4i 2769	. . . . 5 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) = ((𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
21		unundi 4104	. . . . 5 ⊢ (𝐴 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = ((𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
22	20, 21	eqtr4i 2769	. . . 4 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) = (𝐴 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
23		unass 4100	. . . . . 6 ⊢ (((𝐴 ∩ 𝐶) ∪ 𝐵) ∪ 𝐵) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∪ 𝐵))
24		undi 4208	. . . . . . . . 9 ⊢ (𝐵 ∪ (𝐴 ∩ 𝐶)) = ((𝐵 ∪ 𝐴) ∩ (𝐵 ∪ 𝐶))
25		uncom 4087	. . . . . . . . 9 ⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = (𝐵 ∪ (𝐴 ∩ 𝐶))
26		undif2 4410	. . . . . . . . . 10 ⊢ (𝐵 ∪ (𝐴 ∖ 𝐵)) = (𝐵 ∪ 𝐴)
27	26	ineq1i 4142	. . . . . . . . 9 ⊢ ((𝐵 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐵 ∪ 𝐶)) = ((𝐵 ∪ 𝐴) ∩ (𝐵 ∪ 𝐶))
28	24, 25, 27	3eqtr4i 2776	. . . . . . . 8 ⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = ((𝐵 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐵 ∪ 𝐶))
29		undi 4208	. . . . . . . 8 ⊢ (𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) = ((𝐵 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐵 ∪ 𝐶))
30	28, 29	eqtr4i 2769	. . . . . . 7 ⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = (𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶))
31		undi 4208	. . . . . . . 8 ⊢ (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))) = ((𝐵 ∪ (𝐵 ∖ 𝐴)) ∩ (𝐵 ∪ (V ∖ 𝐶)))
32		undifabs 4411	. . . . . . . . 9 ⊢ (𝐵 ∪ (𝐵 ∖ 𝐴)) = 𝐵
33	32	ineq1i 4142	. . . . . . . 8 ⊢ ((𝐵 ∪ (𝐵 ∖ 𝐴)) ∩ (𝐵 ∪ (V ∖ 𝐶))) = (𝐵 ∩ (𝐵 ∪ (V ∖ 𝐶)))
34		inabs 4189	. . . . . . . 8 ⊢ (𝐵 ∩ (𝐵 ∪ (V ∖ 𝐶))) = 𝐵
35	31, 33, 34	3eqtrri 2771	. . . . . . 7 ⊢ 𝐵 = (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))
36	30, 35	uneq12i 4095	. . . . . 6 ⊢ (((𝐴 ∩ 𝐶) ∪ 𝐵) ∪ 𝐵) = ((𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
37		unidm 4086	. . . . . . 7 ⊢ (𝐵 ∪ 𝐵) = 𝐵
38	37	uneq2i 4094	. . . . . 6 ⊢ ((𝐴 ∩ 𝐶) ∪ (𝐵 ∪ 𝐵)) = ((𝐴 ∩ 𝐶) ∪ 𝐵)
39	23, 36, 38	3eqtr3ri 2775	. . . . 5 ⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = ((𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
40		uncom 4087	. . . . . . 7 ⊢ (𝐵 ∪ 𝐶) = (𝐶 ∪ 𝐵)
41	40	ineq2i 4143	. . . . . 6 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∪ 𝐵) ∩ (𝐶 ∪ 𝐵))
42		undir 4210	. . . . . 6 ⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ (𝐶 ∪ 𝐵))
43	41, 42	eqtr4i 2769	. . . . 5 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∩ 𝐶) ∪ 𝐵)
44		unundi 4104	. . . . 5 ⊢ (𝐵 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = ((𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
45	39, 43, 44	3eqtr4i 2776	. . . 4 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)) = (𝐵 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
46	22, 45	ineq12i 4144	. . 3 ⊢ (((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) ∩ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶))) = ((𝐴 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) ∩ (𝐵 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))))
47	4, 46	eqtr4i 2769	. 2 ⊢ ((𝐴 ∩ 𝐵) ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = (((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) ∩ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)))
48	1, 3, 47	3eqtr4i 2776	1 ⊢ if(𝜑, 𝐴, 𝐵) = ((𝐴 ∩ 𝐵) ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))

Syntax hints:   = wceq 1539  {cab 2715  Vcvv 3432   ∖ cdif 3884   ∪ cun 3885   ∩ cin 3886  ifcif 4459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460

This theorem is referenced by: (None)