Metamath Proof Explorer

Theorem dfif4

Description: Alternate definition of the conditional operator df-if . Note that ph is independent of x i.e. a constant true or false. (Contributed by NM, 25-Aug-2013)

Ref Expression
Hypothesis dfif3.1 
|- C = { x | ph }
Assertion dfif4 
|- if ( ph , A , B ) = ( ( A u. B ) i^i ( ( A u. ( _V \ C ) ) i^i ( B u. C ) ) )

Proof

Step Hyp Ref Expression
1 dfif3.1 
 |-  C = { x | ph }
2 1 dfif3 
 |-  if ( ph , A , B ) = ( ( A i^i C ) u. ( B i^i ( _V \ C ) ) )
3 undir 
 |-  ( ( A i^i C ) u. ( B i^i ( _V \ C ) ) ) = ( ( A u. ( B i^i ( _V \ C ) ) ) i^i ( C u. ( B i^i ( _V \ C ) ) ) )
4 undi 
 |-  ( A u. ( B i^i ( _V \ C ) ) ) = ( ( A u. B ) i^i ( A u. ( _V \ C ) ) )
5 undi 
 |-  ( C u. ( B i^i ( _V \ C ) ) ) = ( ( C u. B ) i^i ( C u. ( _V \ C ) ) )
6 uncom 
 |-  ( C u. B ) = ( B u. C )
7 unvdif 
 |-  ( C u. ( _V \ C ) ) = _V
8 6 7 ineq12i 
 |-  ( ( C u. B ) i^i ( C u. ( _V \ C ) ) ) = ( ( B u. C ) i^i _V )
9 inv1 
 |-  ( ( B u. C ) i^i _V ) = ( B u. C )
10 5 8 9 3eqtri 
 |-  ( C u. ( B i^i ( _V \ C ) ) ) = ( B u. C )
11 4 10 ineq12i 
 |-  ( ( A u. ( B i^i ( _V \ C ) ) ) i^i ( C u. ( B i^i ( _V \ C ) ) ) ) = ( ( ( A u. B ) i^i ( A u. ( _V \ C ) ) ) i^i ( B u. C ) )
12 inass 
 |-  ( ( ( 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 ( B u. C ) ) )
13 11 12 eqtri 
 |-  ( ( A u. ( B i^i ( _V \ C ) ) ) i^i ( C u. ( B i^i ( _V \ C ) ) ) ) = ( ( A u. B ) i^i ( ( A u. ( _V \ C ) ) i^i ( B u. C ) ) )
14 2 3 13 3eqtri 
 |-  if ( ph , A , B ) = ( ( A u. B ) i^i ( ( A u. ( _V \ C ) ) i^i ( B u. C ) ) )