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=\left\{x|\phi \right\}$$
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		dfif3.1	$$⊢C=\left\{x|\phi \right\}$$
2	1	dfif3	$$⊢if\left(\phi ,A,B\right)=\left(A\cap C\right)\cup \left(B\cap \left(\mathrm{V}\setminus C\right)\right)$$
3		undir	$$⊢\left(A\cap C\right)\cup \left(B\cap \left(\mathrm{V}\setminus C\right)\right)=\left(A\cup \left(B\cap \left(\mathrm{V}\setminus C\right)\right)\right)\cap \left(C\cup \left(B\cap \left(\mathrm{V}\setminus C\right)\right)\right)$$
4		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)$$
5		undi	$$⊢C\cup \left(B\cap \left(\mathrm{V}\setminus C\right)\right)=\left(C\cup B\right)\cap \left(C\cup \left(\mathrm{V}\setminus C\right)\right)$$
6		uncom	$$⊢C\cup B=B\cup C$$
7		unvdif	$$⊢C\cup \left(\mathrm{V}\setminus C\right)=\mathrm{V}$$
8	6 7	ineq12i	$$⊢\left(C\cup B\right)\cap \left(C\cup \left(\mathrm{V}\setminus C\right)\right)=\left(B\cup C\right)\cap \mathrm{V}$$
9		inv1	$$⊢\left(B\cup C\right)\cap \mathrm{V}=B\cup C$$
10	5 8 9	3eqtri	$$⊢C\cup \left(B\cap \left(\mathrm{V}\setminus C\right)\right)=B\cup C$$
11	4 10	ineq12i	$$⊢\left(A\cup \left(B\cap \left(\mathrm{V}\setminus C\right)\right)\right)\cap \left(C\cup \left(B\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(B\cup C\right)$$
12		inass	$$⊢\left(\left(A\cup B\right)\cap \left(A\cup \left(\mathrm{V}\setminus C\right)\right)\right)\cap \left(B\cup C\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)$$
13	11 12	eqtri	$$⊢\left(A\cup \left(B\cap \left(\mathrm{V}\setminus C\right)\right)\right)\cap \left(C\cup \left(B\cap \left(\mathrm{V}\setminus C\right)\right)\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)$$
14	2 3 13	3eqtri	$$⊢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)$$