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

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 ⊢ 𝐶 = { 𝑥 ∣ 𝜑 }
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 ∖ 𝐶 ) ) ∩ ( 𝐵 ∪ 𝐶 ) ) )