Theorem dfif5 4485

Description: Alternate definition of the conditional operator df-if 4470. Note that 𝜑 is independent of 𝑥 i.e. a constant true or false (see also ab0orv 4337). (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 4205	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((𝐴 ∪ (V ∖ 𝐶)) ∩ (𝐵 ∪ 𝐶))) = (((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) ∩ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)))
2		dfif3.1	. . 3 ⊢ 𝐶 = {𝑥 ∣ 𝜑}
3	2	dfif4 4484	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((𝐴 ∪ (V ∖ 𝐶)) ∩ (𝐵 ∪ 𝐶)))
4		undir 4255	. . 3 ⊢ ((𝐴 ∩ 𝐵) ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = ((𝐴 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) ∩ (𝐵 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))))
5		unidm 4130	. . . . . . . 8 ⊢ (𝐴 ∪ 𝐴) = 𝐴
6	5	uneq1i 4137	. . . . . . 7 ⊢ ((𝐴 ∪ 𝐴) ∪ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶)))
7		unass 4144	. . . . . . 7 ⊢ ((𝐴 ∪ 𝐴) ∪ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∪ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))))
8		undi 4253	. . . . . . 7 ⊢ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶)))
9	6, 7, 8	3eqtr3ri 2855	. . . . . 6 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) = (𝐴 ∪ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))))
10		undi 4253	. . . . . . . 8 ⊢ (𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) = ((𝐴 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐴 ∪ 𝐶))
11		undifabs 4428	. . . . . . . . 9 ⊢ (𝐴 ∪ (𝐴 ∖ 𝐵)) = 𝐴
12	11	ineq1i 4187	. . . . . . . 8 ⊢ ((𝐴 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐴 ∪ 𝐶)) = (𝐴 ∩ (𝐴 ∪ 𝐶))
13		inabs 4234	. . . . . . . 8 ⊢ (𝐴 ∩ (𝐴 ∪ 𝐶)) = 𝐴
14	10, 12, 13	3eqtri 2850	. . . . . . 7 ⊢ (𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) = 𝐴
15		undif2 4427	. . . . . . . . 9 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
16	15	ineq1i 4187	. . . . . . . 8 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) ∩ (𝐴 ∪ (V ∖ 𝐶))) = ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶)))
17		undi 4253	. . . . . . . 8 ⊢ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))) = ((𝐴 ∪ (𝐵 ∖ 𝐴)) ∩ (𝐴 ∪ (V ∖ 𝐶)))
18	16, 17, 8	3eqtr4i 2856	. . . . . . 7 ⊢ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))) = (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶)))
19	14, 18	uneq12i 4139	. . . . . 6 ⊢ ((𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = (𝐴 ∪ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))))
20	9, 19	eqtr4i 2849	. . . . 5 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) = ((𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
21		unundi 4148	. . . . 5 ⊢ (𝐴 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = ((𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
22	20, 21	eqtr4i 2849	. . . 4 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) = (𝐴 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
23		unass 4144	. . . . . 6 ⊢ (((𝐴 ∩ 𝐶) ∪ 𝐵) ∪ 𝐵) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∪ 𝐵))
24		undi 4253	. . . . . . . . 9 ⊢ (𝐵 ∪ (𝐴 ∩ 𝐶)) = ((𝐵 ∪ 𝐴) ∩ (𝐵 ∪ 𝐶))
25		uncom 4131	. . . . . . . . 9 ⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = (𝐵 ∪ (𝐴 ∩ 𝐶))
26		undif2 4427	. . . . . . . . . 10 ⊢ (𝐵 ∪ (𝐴 ∖ 𝐵)) = (𝐵 ∪ 𝐴)
27	26	ineq1i 4187	. . . . . . . . 9 ⊢ ((𝐵 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐵 ∪ 𝐶)) = ((𝐵 ∪ 𝐴) ∩ (𝐵 ∪ 𝐶))
28	24, 25, 27	3eqtr4i 2856	. . . . . . . 8 ⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = ((𝐵 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐵 ∪ 𝐶))
29		undi 4253	. . . . . . . 8 ⊢ (𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) = ((𝐵 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐵 ∪ 𝐶))
30	28, 29	eqtr4i 2849	. . . . . . 7 ⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = (𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶))
31		undi 4253	. . . . . . . 8 ⊢ (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))) = ((𝐵 ∪ (𝐵 ∖ 𝐴)) ∩ (𝐵 ∪ (V ∖ 𝐶)))
32		undifabs 4428	. . . . . . . . 9 ⊢ (𝐵 ∪ (𝐵 ∖ 𝐴)) = 𝐵
33	32	ineq1i 4187	. . . . . . . 8 ⊢ ((𝐵 ∪ (𝐵 ∖ 𝐴)) ∩ (𝐵 ∪ (V ∖ 𝐶))) = (𝐵 ∩ (𝐵 ∪ (V ∖ 𝐶)))
34		inabs 4234	. . . . . . . 8 ⊢ (𝐵 ∩ (𝐵 ∪ (V ∖ 𝐶))) = 𝐵
35	31, 33, 34	3eqtrri 2851	. . . . . . 7 ⊢ 𝐵 = (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))
36	30, 35	uneq12i 4139	. . . . . 6 ⊢ (((𝐴 ∩ 𝐶) ∪ 𝐵) ∪ 𝐵) = ((𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
37		unidm 4130	. . . . . . 7 ⊢ (𝐵 ∪ 𝐵) = 𝐵
38	37	uneq2i 4138	. . . . . 6 ⊢ ((𝐴 ∩ 𝐶) ∪ (𝐵 ∪ 𝐵)) = ((𝐴 ∩ 𝐶) ∪ 𝐵)
39	23, 36, 38	3eqtr3ri 2855	. . . . 5 ⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = ((𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
40		uncom 4131	. . . . . . 7 ⊢ (𝐵 ∪ 𝐶) = (𝐶 ∪ 𝐵)
41	40	ineq2i 4188	. . . . . 6 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∪ 𝐵) ∩ (𝐶 ∪ 𝐵))
42		undir 4255	. . . . . 6 ⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ (𝐶 ∪ 𝐵))
43	41, 42	eqtr4i 2849	. . . . 5 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∩ 𝐶) ∪ 𝐵)
44		unundi 4148	. . . . 5 ⊢ (𝐵 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = ((𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
45	39, 43, 44	3eqtr4i 2856	. . . 4 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)) = (𝐵 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
46	22, 45	ineq12i 4189	. . 3 ⊢ (((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) ∩ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶))) = ((𝐴 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) ∩ (𝐵 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))))
47	4, 46	eqtr4i 2849	. 2 ⊢ ((𝐴 ∩ 𝐵) ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = (((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) ∩ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)))
48	1, 3, 47	3eqtr4i 2856	1 ⊢ if(𝜑, 𝐴, 𝐵) = ((𝐴 ∩ 𝐵) ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))

Syntax hints:   = wceq 1537  {cab 2801  Vcvv 3496   ∖ cdif 3935   ∪ cun 3936   ∩ cin 3937  ifcif 4469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470

This theorem is referenced by: (None)