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		notab	|- { y | -. ph } = ( _V \ { y | ph } )
11	5	difeq2i	|- ( _V \ C ) = ( _V \ { y | ph } )
12	10 11	eqtr4i	|- { y | -. ph } = ( _V \ C )
13	12	ineq2i	|- ( B i^i { y | -. ph } ) = ( B i^i ( _V \ C ) )
14	9 13	eqtr2i	|- ( B i^i ( _V \ C ) ) = { y e. B | -. ph }
15	8 14	uneq12i	|- ( ( A i^i C ) u. ( B i^i ( _V \ C ) ) ) = ( { y e. A | ph } u. { y e. B | -. ph } )
16	2 15	eqtr4i	|- if ( ph , A , B ) = ( ( A i^i C ) u. ( B i^i ( _V \ C ) ) )