This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfif2

Description: An alternate definition of the conditional operator df-if with one fewer connectives (but probably less intuitive to understand). (Contributed by NM, 30-Jan-2006)

		Ref	Expression
	Assertion	dfif2	$⊢ if (φ, A, B) = \{x \| ((x \in B \to φ) \to (x \in A \land φ))\}$

Proof

Step	Hyp	Ref	Expression
1		df-if	$⊢ if (φ, A, B) = \{x \| ((x \in A \land φ) \lor (x \in B \land \neg φ))\}$
2		df-or	$⊢ ((x \in B \land \neg φ) \lor (x \in A \land φ)) \leftrightarrow (\neg (x \in B \land \neg φ) \to (x \in A \land φ))$
3		orcom	$⊢ ((x \in A \land φ) \lor (x \in B \land \neg φ)) \leftrightarrow ((x \in B \land \neg φ) \lor (x \in A \land φ))$
4		iman	$⊢ (x \in B \to φ) \leftrightarrow \neg (x \in B \land \neg φ)$
5	4	imbi1i	$⊢ ((x \in B \to φ) \to (x \in A \land φ)) \leftrightarrow (\neg (x \in B \land \neg φ) \to (x \in A \land φ))$
6	2 3 5	3bitr4i	$⊢ ((x \in A \land φ) \lor (x \in B \land \neg φ)) \leftrightarrow ((x \in B \to φ) \to (x \in A \land φ))$
7	6	abbii	$⊢ \{x \| ((x \in A \land φ) \lor (x \in B \land \neg φ))\} = \{x \| ((x \in B \to φ) \to (x \in A \land φ))\}$
8	1 7	eqtri	$⊢ if (φ, A, B) = \{x \| ((x \in B \to φ) \to (x \in A \land φ))\}$