This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) )