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 ⊢ C = x | φ
Assertion dfif4 ⊢ if φ A B = A ∪ B ∩ A ∪ V ∖ C ∩ B ∪ C

Proof

Step Hyp Ref Expression
1 dfif3.1 ⊢ C = x | φ
2 1 dfif3 ⊢ if φ A B = A ∩ C ∪ B ∩ V ∖ C
3 undir ⊢ A ∩ C ∪ B ∩ V ∖ C = A ∪ B ∩ V ∖ C ∩ C ∪ B ∩ V ∖ C
4 undi ⊢ A ∪ B ∩ V ∖ C = A ∪ B ∩ A ∪ V ∖ C
5 undi ⊢ C ∪ B ∩ V ∖ C = C ∪ B ∩ C ∪ V ∖ C
6 uncom ⊢ C ∪ B = B ∪ C
7 unvdif ⊢ C ∪ V ∖ C = V
8 6 7 ineq12i ⊢ C ∪ B ∩ C ∪ V ∖ C = B ∪ C ∩ V
9 inv1 ⊢ B ∪ C ∩ V = B ∪ C
10 5 8 9 3eqtri ⊢ C ∪ B ∩ V ∖ C = B ∪ C
11 4 10 ineq12i ⊢ A ∪ B ∩ V ∖ C ∩ C ∪ B ∩ V ∖ C = A ∪ B ∩ A ∪ V ∖ C ∩ B ∪ C
12 inass ⊢ A ∪ B ∩ A ∪ V ∖ C ∩ B ∪ C = A ∪ B ∩ A ∪ V ∖ C ∩ B ∪ C
13 11 12 eqtri ⊢ A ∪ B ∩ V ∖ C ∩ C ∪ B ∩ V ∖ C = A ∪ B ∩ A ∪ V ∖ C ∩ B ∪ C
14 2 3 13 3eqtri ⊢ if φ A B = A ∪ B ∩ A ∪ V ∖ C ∩ B ∪ C