Theorem dfif5 4538

Description: Alternate definition of the conditional operator df-if 4523. Note that 𝜑 is independent of 𝑥 i.e. a constant true or false (see also ab0orv 4374). (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 4222	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((𝐴 ∪ (V ∖ 𝐶)) ∩ (𝐵 ∪ 𝐶))) = (((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) ∩ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)))
2		dfif3.1	. . 3 ⊢ 𝐶 = {𝑥 ∣ 𝜑}
3	2	dfif4 4537	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((𝐴 ∪ (V ∖ 𝐶)) ∩ (𝐵 ∪ 𝐶)))
4		undir 4272	. . 3 ⊢ ((𝐴 ∩ 𝐵) ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = ((𝐴 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) ∩ (𝐵 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))))
5		unidm 4148	. . . . . . . 8 ⊢ (𝐴 ∪ 𝐴) = 𝐴
6	5	uneq1i 4155	. . . . . . 7 ⊢ ((𝐴 ∪ 𝐴) ∪ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶)))
7		unass 4162	. . . . . . 7 ⊢ ((𝐴 ∪ 𝐴) ∪ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∪ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))))
8		undi 4270	. . . . . . 7 ⊢ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶)))
9	6, 7, 8	3eqtr3ri 2768	. . . . . 6 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) = (𝐴 ∪ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))))
10		undi 4270	. . . . . . . 8 ⊢ (𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) = ((𝐴 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐴 ∪ 𝐶))
11		undifabs 4473	. . . . . . . . 9 ⊢ (𝐴 ∪ (𝐴 ∖ 𝐵)) = 𝐴
12	11	ineq1i 4204	. . . . . . . 8 ⊢ ((𝐴 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐴 ∪ 𝐶)) = (𝐴 ∩ (𝐴 ∪ 𝐶))
13		inabs 4251	. . . . . . . 8 ⊢ (𝐴 ∩ (𝐴 ∪ 𝐶)) = 𝐴
14	10, 12, 13	3eqtri 2763	. . . . . . 7 ⊢ (𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) = 𝐴
15		undif2 4472	. . . . . . . . 9 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
16	15	ineq1i 4204	. . . . . . . 8 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) ∩ (𝐴 ∪ (V ∖ 𝐶))) = ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶)))
17		undi 4270	. . . . . . . 8 ⊢ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))) = ((𝐴 ∪ (𝐵 ∖ 𝐴)) ∩ (𝐴 ∪ (V ∖ 𝐶)))
18	16, 17, 8	3eqtr4i 2769	. . . . . . 7 ⊢ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))) = (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶)))
19	14, 18	uneq12i 4157	. . . . . 6 ⊢ ((𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = (𝐴 ∪ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))))
20	9, 19	eqtr4i 2762	. . . . 5 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) = ((𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
21		unundi 4166	. . . . 5 ⊢ (𝐴 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = ((𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
22	20, 21	eqtr4i 2762	. . . 4 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) = (𝐴 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
23		unass 4162	. . . . . 6 ⊢ (((𝐴 ∩ 𝐶) ∪ 𝐵) ∪ 𝐵) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∪ 𝐵))
24		undi 4270	. . . . . . . . 9 ⊢ (𝐵 ∪ (𝐴 ∩ 𝐶)) = ((𝐵 ∪ 𝐴) ∩ (𝐵 ∪ 𝐶))
25		uncom 4149	. . . . . . . . 9 ⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = (𝐵 ∪ (𝐴 ∩ 𝐶))
26		undif2 4472	. . . . . . . . . 10 ⊢ (𝐵 ∪ (𝐴 ∖ 𝐵)) = (𝐵 ∪ 𝐴)
27	26	ineq1i 4204	. . . . . . . . 9 ⊢ ((𝐵 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐵 ∪ 𝐶)) = ((𝐵 ∪ 𝐴) ∩ (𝐵 ∪ 𝐶))
28	24, 25, 27	3eqtr4i 2769	. . . . . . . 8 ⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = ((𝐵 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐵 ∪ 𝐶))
29		undi 4270	. . . . . . . 8 ⊢ (𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) = ((𝐵 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐵 ∪ 𝐶))
30	28, 29	eqtr4i 2762	. . . . . . 7 ⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = (𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶))
31		undi 4270	. . . . . . . 8 ⊢ (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))) = ((𝐵 ∪ (𝐵 ∖ 𝐴)) ∩ (𝐵 ∪ (V ∖ 𝐶)))
32		undifabs 4473	. . . . . . . . 9 ⊢ (𝐵 ∪ (𝐵 ∖ 𝐴)) = 𝐵
33	32	ineq1i 4204	. . . . . . . 8 ⊢ ((𝐵 ∪ (𝐵 ∖ 𝐴)) ∩ (𝐵 ∪ (V ∖ 𝐶))) = (𝐵 ∩ (𝐵 ∪ (V ∖ 𝐶)))
34		inabs 4251	. . . . . . . 8 ⊢ (𝐵 ∩ (𝐵 ∪ (V ∖ 𝐶))) = 𝐵
35	31, 33, 34	3eqtrri 2764	. . . . . . 7 ⊢ 𝐵 = (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))
36	30, 35	uneq12i 4157	. . . . . 6 ⊢ (((𝐴 ∩ 𝐶) ∪ 𝐵) ∪ 𝐵) = ((𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
37		unidm 4148	. . . . . . 7 ⊢ (𝐵 ∪ 𝐵) = 𝐵
38	37	uneq2i 4156	. . . . . 6 ⊢ ((𝐴 ∩ 𝐶) ∪ (𝐵 ∪ 𝐵)) = ((𝐴 ∩ 𝐶) ∪ 𝐵)
39	23, 36, 38	3eqtr3ri 2768	. . . . 5 ⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = ((𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
40		uncom 4149	. . . . . . 7 ⊢ (𝐵 ∪ 𝐶) = (𝐶 ∪ 𝐵)
41	40	ineq2i 4205	. . . . . 6 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∪ 𝐵) ∩ (𝐶 ∪ 𝐵))
42		undir 4272	. . . . . 6 ⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ (𝐶 ∪ 𝐵))
43	41, 42	eqtr4i 2762	. . . . 5 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∩ 𝐶) ∪ 𝐵)
44		unundi 4166	. . . . 5 ⊢ (𝐵 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = ((𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
45	39, 43, 44	3eqtr4i 2769	. . . 4 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)) = (𝐵 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
46	22, 45	ineq12i 4206	. . 3 ⊢ (((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) ∩ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶))) = ((𝐴 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) ∩ (𝐵 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))))
47	4, 46	eqtr4i 2762	. 2 ⊢ ((𝐴 ∩ 𝐵) ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = (((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) ∩ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)))
48	1, 3, 47	3eqtr4i 2769	1 ⊢ if(𝜑, 𝐴, 𝐵) = ((𝐴 ∩ 𝐵) ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))

Syntax hints:   = wceq 1541  {cab 2708  Vcvv 3473   ∖ cdif 3941   ∪ cun 3942   ∩ cin 3943  ifcif 4522

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523

This theorem is referenced by: (None)