Theorem dfif5 4471

Description: Alternate definition of the conditional operator df-if 4455. Note that 𝜑 is independent of 𝑥 i.e. a constant true or false (see also ab0orv 4311). (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 4163	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((𝐴 ∪ (V ∖ 𝐶)) ∩ (𝐵 ∪ 𝐶))) = (((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) ∩ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)))
2		dfif3.1	. . 3 ⊢ 𝐶 = {𝑥 ∣ 𝜑}
3	2	dfif4 4470	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((𝐴 ∪ (V ∖ 𝐶)) ∩ (𝐵 ∪ 𝐶)))
4		undir 4215	. . 3 ⊢ ((𝐴 ∩ 𝐵) ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = ((𝐴 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) ∩ (𝐵 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))))
5		unidm 4087	. . . . . . . 8 ⊢ (𝐴 ∪ 𝐴) = 𝐴
6	5	uneq1i 4094	. . . . . . 7 ⊢ ((𝐴 ∪ 𝐴) ∪ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶)))
7		unass 4101	. . . . . . 7 ⊢ ((𝐴 ∪ 𝐴) ∪ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∪ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))))
8		undi 4213	. . . . . . 7 ⊢ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶)))
9	6, 7, 8	3eqtr3ri 2771	. . . . . 6 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) = (𝐴 ∪ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))))
10		undi 4213	. . . . . . . 8 ⊢ (𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) = ((𝐴 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐴 ∪ 𝐶))
11		undifabs 4406	. . . . . . . . 9 ⊢ (𝐴 ∪ (𝐴 ∖ 𝐵)) = 𝐴
12	11	ineq1i 4145	. . . . . . . 8 ⊢ ((𝐴 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐴 ∪ 𝐶)) = (𝐴 ∩ (𝐴 ∪ 𝐶))
13		inabs 4194	. . . . . . . 8 ⊢ (𝐴 ∩ (𝐴 ∪ 𝐶)) = 𝐴
14	10, 12, 13	3eqtri 2766	. . . . . . 7 ⊢ (𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) = 𝐴
15		undif2 4405	. . . . . . . . 9 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
16	15	ineq1i 4145	. . . . . . . 8 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) ∩ (𝐴 ∪ (V ∖ 𝐶))) = ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶)))
17		undi 4213	. . . . . . . 8 ⊢ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))) = ((𝐴 ∪ (𝐵 ∖ 𝐴)) ∩ (𝐴 ∪ (V ∖ 𝐶)))
18	16, 17, 8	3eqtr4i 2772	. . . . . . 7 ⊢ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))) = (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶)))
19	14, 18	uneq12i 4096	. . . . . 6 ⊢ ((𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = (𝐴 ∪ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))))
20	9, 19	eqtr4i 2765	. . . . 5 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) = ((𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
21		unundi 4105	. . . . 5 ⊢ (𝐴 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = ((𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
22	20, 21	eqtr4i 2765	. . . 4 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) = (𝐴 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
23		unass 4101	. . . . . 6 ⊢ (((𝐴 ∩ 𝐶) ∪ 𝐵) ∪ 𝐵) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∪ 𝐵))
24		undi 4213	. . . . . . . . 9 ⊢ (𝐵 ∪ (𝐴 ∩ 𝐶)) = ((𝐵 ∪ 𝐴) ∩ (𝐵 ∪ 𝐶))
25		uncom 4088	. . . . . . . . 9 ⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = (𝐵 ∪ (𝐴 ∩ 𝐶))
26		undif2 4405	. . . . . . . . . 10 ⊢ (𝐵 ∪ (𝐴 ∖ 𝐵)) = (𝐵 ∪ 𝐴)
27	26	ineq1i 4145	. . . . . . . . 9 ⊢ ((𝐵 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐵 ∪ 𝐶)) = ((𝐵 ∪ 𝐴) ∩ (𝐵 ∪ 𝐶))
28	24, 25, 27	3eqtr4i 2772	. . . . . . . 8 ⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = ((𝐵 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐵 ∪ 𝐶))
29		undi 4213	. . . . . . . 8 ⊢ (𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) = ((𝐵 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐵 ∪ 𝐶))
30	28, 29	eqtr4i 2765	. . . . . . 7 ⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = (𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶))
31		undi 4213	. . . . . . . 8 ⊢ (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))) = ((𝐵 ∪ (𝐵 ∖ 𝐴)) ∩ (𝐵 ∪ (V ∖ 𝐶)))
32		undifabs 4406	. . . . . . . . 9 ⊢ (𝐵 ∪ (𝐵 ∖ 𝐴)) = 𝐵
33	32	ineq1i 4145	. . . . . . . 8 ⊢ ((𝐵 ∪ (𝐵 ∖ 𝐴)) ∩ (𝐵 ∪ (V ∖ 𝐶))) = (𝐵 ∩ (𝐵 ∪ (V ∖ 𝐶)))
34		inabs 4194	. . . . . . . 8 ⊢ (𝐵 ∩ (𝐵 ∪ (V ∖ 𝐶))) = 𝐵
35	31, 33, 34	3eqtrri 2767	. . . . . . 7 ⊢ 𝐵 = (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))
36	30, 35	uneq12i 4096	. . . . . 6 ⊢ (((𝐴 ∩ 𝐶) ∪ 𝐵) ∪ 𝐵) = ((𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
37		unidm 4087	. . . . . . 7 ⊢ (𝐵 ∪ 𝐵) = 𝐵
38	37	uneq2i 4095	. . . . . 6 ⊢ ((𝐴 ∩ 𝐶) ∪ (𝐵 ∪ 𝐵)) = ((𝐴 ∩ 𝐶) ∪ 𝐵)
39	23, 36, 38	3eqtr3ri 2771	. . . . 5 ⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = ((𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
40		uncom 4088	. . . . . . 7 ⊢ (𝐵 ∪ 𝐶) = (𝐶 ∪ 𝐵)
41	40	ineq2i 4146	. . . . . 6 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∪ 𝐵) ∩ (𝐶 ∪ 𝐵))
42		undir 4215	. . . . . 6 ⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ (𝐶 ∪ 𝐵))
43	41, 42	eqtr4i 2765	. . . . 5 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∩ 𝐶) ∪ 𝐵)
44		unundi 4105	. . . . 5 ⊢ (𝐵 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = ((𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
45	39, 43, 44	3eqtr4i 2772	. . . 4 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)) = (𝐵 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))
46	22, 45	ineq12i 4147	. . 3 ⊢ (((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) ∩ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶))) = ((𝐴 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) ∩ (𝐵 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))))
47	4, 46	eqtr4i 2765	. 2 ⊢ ((𝐴 ∩ 𝐵) ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = (((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) ∩ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)))
48	1, 3, 47	3eqtr4i 2772	1 ⊢ if(𝜑, 𝐴, 𝐵) = ((𝐴 ∩ 𝐵) ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))

Syntax hints:   = wceq 1547  {cab 2717  Vcvv 3431   ∖ cdif 3880   ∪ cun 3881   ∩ cin 3882  ifcif 4454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455

This theorem is referenced by: (None)