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\left(\phi ,B,C\right)\leftrightarrow \left(\left(\phi \to A=B\right)\wedge \left(\neg \phi \to A=C\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqif	$$⊢A=if\left(\phi ,B,C\right)\leftrightarrow \left(\left(\phi \wedge A=B\right)\vee \left(\neg \phi \wedge A=C\right)\right)$$
2		cases2	$$⊢\left(\left(\phi \wedge A=B\right)\vee \left(\neg \phi \wedge A=C\right)\right)\leftrightarrow \left(\left(\phi \to A=B\right)\wedge \left(\neg \phi \to A=C\right)\right)$$
3	1 2	bitri	$$⊢A=if\left(\phi ,B,C\right)\leftrightarrow \left(\left(\phi \to A=B\right)\wedge \left(\neg \phi \to A=C\right)\right)$$