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	⊢ 𝐶 = { 𝑥 ∣ 𝜑 }
Assertion	dfif4	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = ( ( 𝐴 ∪ 𝐵 ) ∩ ( ( 𝐴 ∪ ( V ∖ 𝐶 ) ) ∩ ( 𝐵 ∪ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfif3.1	⊢ 𝐶 = { 𝑥 ∣ 𝜑 }
2	1	dfif3	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = ( ( 𝐴 ∩ 𝐶 ) ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) )
3		undir	⊢ ( ( 𝐴 ∩ 𝐶 ) ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) = ( ( 𝐴 ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) ∩ ( 𝐶 ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) )
4		undi	⊢ ( 𝐴 ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) = ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐴 ∪ ( V ∖ 𝐶 ) ) )
5		undi	⊢ ( 𝐶 ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) = ( ( 𝐶 ∪ 𝐵 ) ∩ ( 𝐶 ∪ ( V ∖ 𝐶 ) ) )
6		uncom	⊢ ( 𝐶 ∪ 𝐵 ) = ( 𝐵 ∪ 𝐶 )
7		unvdif	⊢ ( 𝐶 ∪ ( V ∖ 𝐶 ) ) = V
8	6 7	ineq12i	⊢ ( ( 𝐶 ∪ 𝐵 ) ∩ ( 𝐶 ∪ ( V ∖ 𝐶 ) ) ) = ( ( 𝐵 ∪ 𝐶 ) ∩ V )
9		inv1	⊢ ( ( 𝐵 ∪ 𝐶 ) ∩ V ) = ( 𝐵 ∪ 𝐶 )
10	5 8 9	3eqtri	⊢ ( 𝐶 ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) = ( 𝐵 ∪ 𝐶 )
11	4 10	ineq12i	⊢ ( ( 𝐴 ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) ∩ ( 𝐶 ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) ) = ( ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐴 ∪ ( V ∖ 𝐶 ) ) ) ∩ ( 𝐵 ∪ 𝐶 ) )
12		inass	⊢ ( ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐴 ∪ ( V ∖ 𝐶 ) ) ) ∩ ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐴 ∪ 𝐵 ) ∩ ( ( 𝐴 ∪ ( V ∖ 𝐶 ) ) ∩ ( 𝐵 ∪ 𝐶 ) ) )
13	11 12	eqtri	⊢ ( ( 𝐴 ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) ∩ ( 𝐶 ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) ) = ( ( 𝐴 ∪ 𝐵 ) ∩ ( ( 𝐴 ∪ ( V ∖ 𝐶 ) ) ∩ ( 𝐵 ∪ 𝐶 ) ) )
14	2 3 13	3eqtri	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = ( ( 𝐴 ∪ 𝐵 ) ∩ ( ( 𝐴 ∪ ( V ∖ 𝐶 ) ) ∩ ( 𝐵 ∪ 𝐶 ) ) )