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

Metamath Proof Explorer

Theorem dfif3

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) (Revised by Mario Carneiro, 8-Sep-2013)

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

Proof

Step Hyp Ref Expression
1 dfif3.1 
 |-  C = { x | ph }
2 dfif6 
 |-  if ( ph , A , B ) = ( { y e. A | ph } u. { y e. B | -. ph } )
3 biidd 
 |-  ( x = y -> ( ph <-> ph ) )
4 3 cbvabv 
 |-  { x | ph } = { y | ph }
5 1 4 eqtri 
 |-  C = { y | ph }
6 5 ineq2i 
 |-  ( A i^i C ) = ( A i^i { y | ph } )
7 dfrab3 
 |-  { y e. A | ph } = ( A i^i { y | ph } )
8 6 7 eqtr4i 
 |-  ( A i^i C ) = { y e. A | ph }
9 dfrab3 
 |-  { y e. B | -. ph } = ( B i^i { y | -. ph } )
10 biidd 
 |-  ( y = z -> ( ph <-> ph ) )
11 10 notabw 
 |-  { y | -. ph } = ( _V \ { z | ph } )
12 biidd 
 |-  ( x = z -> ( ph <-> ph ) )
13 12 cbvabv 
 |-  { x | ph } = { z | ph }
14 1 13 eqtri 
 |-  C = { z | ph }
15 14 difeq2i 
 |-  ( _V \ C ) = ( _V \ { z | ph } )
16 11 15 eqtr4i 
 |-  { y | -. ph } = ( _V \ C )
17 16 ineq2i 
 |-  ( B i^i { y | -. ph } ) = ( B i^i ( _V \ C ) )
18 9 17 eqtr2i 
 |-  ( B i^i ( _V \ C ) ) = { y e. B | -. ph }
19 8 18 uneq12i 
 |-  ( ( A i^i C ) u. ( B i^i ( _V \ C ) ) ) = ( { y e. A | ph } u. { y e. B | -. ph } )
20 2 19 eqtr4i 
 |-  if ( ph , A , B ) = ( ( A i^i C ) u. ( B i^i ( _V \ C ) ) )