Metamath Proof Explorer

Theorem ifval

Description: Another expression of the value of the if predicate, analogous to eqif . See also the more specialized iftrue and iffalse . (Contributed by BJ, 6-Apr-2019)

		Ref	Expression
	Assertion	ifval	$⊢ A = if (φ, B, C) \leftrightarrow ((φ \to A = B) \land (\neg φ \to A = C))$

Proof

Step	Hyp	Ref	Expression
1		eqif	$⊢ A = if (φ, B, C) \leftrightarrow ((φ \land A = B) \lor (\neg φ \land A = C))$
2		cases2	$⊢ ((φ \land A = B) \lor (\neg φ \land A = C)) \leftrightarrow ((φ \to A = B) \land (\neg φ \to A = C))$
3	1 2	bitri	$⊢ A = if (φ, B, C) \leftrightarrow ((φ \to A = B) \land (\neg φ \to A = C))$