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 = { x | ph }
Assertion	dfif5	|- if ( ph , A , B ) = ( ( A i^i B ) u. ( ( ( A \ B ) i^i C ) u. ( ( B \ A ) i^i ( _V \ C ) ) ) )

Proof

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