# Metamath Proof Explorer

## Theorem dfif5

Description: Alternate definition of the conditional operator df-if . Note that ph is independent of x i.e. a constant true or false (see also ab0orv ). (Contributed by Gérard Lang, 18-Aug-2013)

Ref Expression
Hypothesis dfif3.1 ${⊢}{C}=\left\{{x}|{\phi }\right\}$
Assertion dfif5 ${⊢}if\left({\phi },{A},{B}\right)=\left({A}\cap {B}\right)\cup \left(\left(\left({A}\setminus {B}\right)\cap {C}\right)\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 dfif3.1 ${⊢}{C}=\left\{{x}|{\phi }\right\}$
2 inindi ${⊢}\left({A}\cup {B}\right)\cap \left(\left({A}\cup \left(\mathrm{V}\setminus {C}\right)\right)\cap \left({B}\cup {C}\right)\right)=\left(\left({A}\cup {B}\right)\cap \left({A}\cup \left(\mathrm{V}\setminus {C}\right)\right)\right)\cap \left(\left({A}\cup {B}\right)\cap \left({B}\cup {C}\right)\right)$
3 1 dfif4 ${⊢}if\left({\phi },{A},{B}\right)=\left({A}\cup {B}\right)\cap \left(\left({A}\cup \left(\mathrm{V}\setminus {C}\right)\right)\cap \left({B}\cup {C}\right)\right)$
4 undir ${⊢}\left({A}\cap {B}\right)\cup \left(\left(\left({A}\setminus {B}\right)\cap {C}\right)\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)=\left({A}\cup \left(\left(\left({A}\setminus {B}\right)\cap {C}\right)\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)\right)\cap \left({B}\cup \left(\left(\left({A}\setminus {B}\right)\cap {C}\right)\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)\right)$
5 unidm ${⊢}{A}\cup {A}={A}$
6 5 uneq1i ${⊢}\left({A}\cup {A}\right)\cup \left({B}\cap \left(\mathrm{V}\setminus {C}\right)\right)={A}\cup \left({B}\cap \left(\mathrm{V}\setminus {C}\right)\right)$
7 unass ${⊢}\left({A}\cup {A}\right)\cup \left({B}\cap \left(\mathrm{V}\setminus {C}\right)\right)={A}\cup \left({A}\cup \left({B}\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)$
8 undi ${⊢}{A}\cup \left({B}\cap \left(\mathrm{V}\setminus {C}\right)\right)=\left({A}\cup {B}\right)\cap \left({A}\cup \left(\mathrm{V}\setminus {C}\right)\right)$
9 6 7 8 3eqtr3ri ${⊢}\left({A}\cup {B}\right)\cap \left({A}\cup \left(\mathrm{V}\setminus {C}\right)\right)={A}\cup \left({A}\cup \left({B}\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)$
10 undi ${⊢}{A}\cup \left(\left({A}\setminus {B}\right)\cap {C}\right)=\left({A}\cup \left({A}\setminus {B}\right)\right)\cap \left({A}\cup {C}\right)$
11 undifabs ${⊢}{A}\cup \left({A}\setminus {B}\right)={A}$
12 11 ineq1i ${⊢}\left({A}\cup \left({A}\setminus {B}\right)\right)\cap \left({A}\cup {C}\right)={A}\cap \left({A}\cup {C}\right)$
13 inabs ${⊢}{A}\cap \left({A}\cup {C}\right)={A}$
14 10 12 13 3eqtri ${⊢}{A}\cup \left(\left({A}\setminus {B}\right)\cap {C}\right)={A}$
15 undif2 ${⊢}{A}\cup \left({B}\setminus {A}\right)={A}\cup {B}$
16 15 ineq1i ${⊢}\left({A}\cup \left({B}\setminus {A}\right)\right)\cap \left({A}\cup \left(\mathrm{V}\setminus {C}\right)\right)=\left({A}\cup {B}\right)\cap \left({A}\cup \left(\mathrm{V}\setminus {C}\right)\right)$
17 undi ${⊢}{A}\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)=\left({A}\cup \left({B}\setminus {A}\right)\right)\cap \left({A}\cup \left(\mathrm{V}\setminus {C}\right)\right)$
18 16 17 8 3eqtr4i ${⊢}{A}\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)={A}\cup \left({B}\cap \left(\mathrm{V}\setminus {C}\right)\right)$
19 14 18 uneq12i ${⊢}\left({A}\cup \left(\left({A}\setminus {B}\right)\cap {C}\right)\right)\cup \left({A}\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)={A}\cup \left({A}\cup \left({B}\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)$
20 9 19 eqtr4i ${⊢}\left({A}\cup {B}\right)\cap \left({A}\cup \left(\mathrm{V}\setminus {C}\right)\right)=\left({A}\cup \left(\left({A}\setminus {B}\right)\cap {C}\right)\right)\cup \left({A}\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)$
21 unundi ${⊢}{A}\cup \left(\left(\left({A}\setminus {B}\right)\cap {C}\right)\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)=\left({A}\cup \left(\left({A}\setminus {B}\right)\cap {C}\right)\right)\cup \left({A}\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)$
22 20 21 eqtr4i ${⊢}\left({A}\cup {B}\right)\cap \left({A}\cup \left(\mathrm{V}\setminus {C}\right)\right)={A}\cup \left(\left(\left({A}\setminus {B}\right)\cap {C}\right)\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)$
23 unass ${⊢}\left(\left({A}\cap {C}\right)\cup {B}\right)\cup {B}=\left({A}\cap {C}\right)\cup \left({B}\cup {B}\right)$
24 undi ${⊢}{B}\cup \left({A}\cap {C}\right)=\left({B}\cup {A}\right)\cap \left({B}\cup {C}\right)$
25 uncom ${⊢}\left({A}\cap {C}\right)\cup {B}={B}\cup \left({A}\cap {C}\right)$
26 undif2 ${⊢}{B}\cup \left({A}\setminus {B}\right)={B}\cup {A}$
27 26 ineq1i ${⊢}\left({B}\cup \left({A}\setminus {B}\right)\right)\cap \left({B}\cup {C}\right)=\left({B}\cup {A}\right)\cap \left({B}\cup {C}\right)$
28 24 25 27 3eqtr4i ${⊢}\left({A}\cap {C}\right)\cup {B}=\left({B}\cup \left({A}\setminus {B}\right)\right)\cap \left({B}\cup {C}\right)$
29 undi ${⊢}{B}\cup \left(\left({A}\setminus {B}\right)\cap {C}\right)=\left({B}\cup \left({A}\setminus {B}\right)\right)\cap \left({B}\cup {C}\right)$
30 28 29 eqtr4i ${⊢}\left({A}\cap {C}\right)\cup {B}={B}\cup \left(\left({A}\setminus {B}\right)\cap {C}\right)$
31 undi ${⊢}{B}\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)=\left({B}\cup \left({B}\setminus {A}\right)\right)\cap \left({B}\cup \left(\mathrm{V}\setminus {C}\right)\right)$
32 undifabs ${⊢}{B}\cup \left({B}\setminus {A}\right)={B}$
33 32 ineq1i ${⊢}\left({B}\cup \left({B}\setminus {A}\right)\right)\cap \left({B}\cup \left(\mathrm{V}\setminus {C}\right)\right)={B}\cap \left({B}\cup \left(\mathrm{V}\setminus {C}\right)\right)$
34 inabs ${⊢}{B}\cap \left({B}\cup \left(\mathrm{V}\setminus {C}\right)\right)={B}$
35 31 33 34 3eqtrri ${⊢}{B}={B}\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)$
36 30 35 uneq12i ${⊢}\left(\left({A}\cap {C}\right)\cup {B}\right)\cup {B}=\left({B}\cup \left(\left({A}\setminus {B}\right)\cap {C}\right)\right)\cup \left({B}\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)$
37 unidm ${⊢}{B}\cup {B}={B}$
38 37 uneq2i ${⊢}\left({A}\cap {C}\right)\cup \left({B}\cup {B}\right)=\left({A}\cap {C}\right)\cup {B}$
39 23 36 38 3eqtr3ri ${⊢}\left({A}\cap {C}\right)\cup {B}=\left({B}\cup \left(\left({A}\setminus {B}\right)\cap {C}\right)\right)\cup \left({B}\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)$
40 uncom ${⊢}{B}\cup {C}={C}\cup {B}$
41 40 ineq2i ${⊢}\left({A}\cup {B}\right)\cap \left({B}\cup {C}\right)=\left({A}\cup {B}\right)\cap \left({C}\cup {B}\right)$
42 undir ${⊢}\left({A}\cap {C}\right)\cup {B}=\left({A}\cup {B}\right)\cap \left({C}\cup {B}\right)$
43 41 42 eqtr4i ${⊢}\left({A}\cup {B}\right)\cap \left({B}\cup {C}\right)=\left({A}\cap {C}\right)\cup {B}$
44 unundi ${⊢}{B}\cup \left(\left(\left({A}\setminus {B}\right)\cap {C}\right)\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)=\left({B}\cup \left(\left({A}\setminus {B}\right)\cap {C}\right)\right)\cup \left({B}\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)$
45 39 43 44 3eqtr4i ${⊢}\left({A}\cup {B}\right)\cap \left({B}\cup {C}\right)={B}\cup \left(\left(\left({A}\setminus {B}\right)\cap {C}\right)\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)$
46 22 45 ineq12i ${⊢}\left(\left({A}\cup {B}\right)\cap \left({A}\cup \left(\mathrm{V}\setminus {C}\right)\right)\right)\cap \left(\left({A}\cup {B}\right)\cap \left({B}\cup {C}\right)\right)=\left({A}\cup \left(\left(\left({A}\setminus {B}\right)\cap {C}\right)\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)\right)\cap \left({B}\cup \left(\left(\left({A}\setminus {B}\right)\cap {C}\right)\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)\right)$
47 4 46 eqtr4i ${⊢}\left({A}\cap {B}\right)\cup \left(\left(\left({A}\setminus {B}\right)\cap {C}\right)\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)=\left(\left({A}\cup {B}\right)\cap \left({A}\cup \left(\mathrm{V}\setminus {C}\right)\right)\right)\cap \left(\left({A}\cup {B}\right)\cap \left({B}\cup {C}\right)\right)$
48 2 3 47 3eqtr4i ${⊢}if\left({\phi },{A},{B}\right)=\left({A}\cap {B}\right)\cup \left(\left(\left({A}\setminus {B}\right)\cap {C}\right)\cup \left(\left({B}\setminus {A}\right)\cap \left(\mathrm{V}\setminus {C}\right)\right)\right)$