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