dfif3

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) (Revised by Mario Carneiro, 8-Sep-2013)

		Ref	Expression
	Hypothesis	dfif3.1	$⊢ C = \{x \| φ\}$
	Assertion	dfif3	$⊢ if (φ, A, B) = (A \cap C) \cup (B \cap (V ∖ C))$

Proof

Step	Hyp	Ref	Expression
1		dfif3.1	$⊢ C = \{x \| φ\}$
2		dfif6	$⊢ if (φ, A, B) = \{y \in A \| φ\} \cup \{y \in B \| \neg φ\}$
3		biidd	$⊢ x = y \to (φ \leftrightarrow φ)$
4	3	cbvabv	$⊢ \{x \| φ\} = \{y \| φ\}$
5	1 4	eqtri	$⊢ C = \{y \| φ\}$
6	5	ineq2i	$⊢ A \cap C = A \cap \{y \| φ\}$
7		dfrab3	$⊢ \{y \in A \| φ\} = A \cap \{y \| φ\}$
8	6 7	eqtr4i	$⊢ A \cap C = \{y \in A \| φ\}$
9		dfrab3	$⊢ \{y \in B \| \neg φ\} = B \cap \{y \| \neg φ\}$
10		biidd	$⊢ y = z \to (φ \leftrightarrow φ)$
11	10	notabw	$⊢ \{y \| \neg φ\} = V ∖ \{z \| φ\}$
12		biidd	$⊢ x = z \to (φ \leftrightarrow φ)$
13	12	cbvabv	$⊢ \{x \| φ\} = \{z \| φ\}$
14	1 13	eqtri	$⊢ C = \{z \| φ\}$
15	14	difeq2i	$⊢ V ∖ C = V ∖ \{z \| φ\}$
16	11 15	eqtr4i	$⊢ \{y \| \neg φ\} = V ∖ C$
17	16	ineq2i	$⊢ B \cap \{y \| \neg φ\} = B \cap (V ∖ C)$
18	9 17	eqtr2i	$⊢ B \cap (V ∖ C) = \{y \in B \| \neg φ\}$
19	8 18	uneq12i	$⊢ (A \cap C) \cup (B \cap (V ∖ C)) = \{y \in A \| φ\} \cup \{y \in B \| \neg φ\}$
20	2 19	eqtr4i	$⊢ if (φ, A, B) = (A \cap C) \cup (B \cap (V ∖ C))$

Metamath Proof Explorer

Theorem dfif3

Proof