Theorem dfif6

Description: An alternate definition of the conditional operator df-if as a simple class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013)

	Ref	Expression
Assertion	dfif6	$$⊢if\left(\phi ,A,B\right)=\left\{x\in A|\phi \right\}\cup \left\{x\in B|\neg \phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		unab	$$⊢\left\{x|\left(x\in A\wedge \phi \right)\right\}\cup \left\{x|\left(x\in B\wedge \neg \phi \right)\right\}=\left\{x|\left(\left(x\in A\wedge \phi \right)\vee \left(x\in B\wedge \neg \phi \right)\right)\right\}$$
2		df-rab	$$⊢\left\{x\in A|\phi \right\}=\left\{x|\left(x\in A\wedge \phi \right)\right\}$$
3		df-rab	$$⊢\left\{x\in B|\neg \phi \right\}=\left\{x|\left(x\in B\wedge \neg \phi \right)\right\}$$
4	2 3	uneq12i	$$⊢\left\{x\in A|\phi \right\}\cup \left\{x\in B|\neg \phi \right\}=\left\{x|\left(x\in A\wedge \phi \right)\right\}\cup \left\{x|\left(x\in B\wedge \neg \phi \right)\right\}$$
5		df-if	$$⊢if\left(\phi ,A,B\right)=\left\{x|\left(\left(x\in A\wedge \phi \right)\vee \left(x\in B\wedge \neg \phi \right)\right)\right\}$$
6	1 4 5	3eqtr4ri	$$⊢if\left(\phi ,A,B\right)=\left\{x\in A|\phi \right\}\cup \left\{x\in B|\neg \phi \right\}$$