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	⊢ ( 𝐴 = if ( 𝜑 , 𝐵 , 𝐶 ) ↔ ( ( 𝜑 → 𝐴 = 𝐵 ) ∧ ( ¬ 𝜑 → 𝐴 = 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqif	⊢ ( 𝐴 = if ( 𝜑 , 𝐵 , 𝐶 ) ↔ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∨ ( ¬ 𝜑 ∧ 𝐴 = 𝐶 ) ) )
2		cases2	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∨ ( ¬ 𝜑 ∧ 𝐴 = 𝐶 ) ) ↔ ( ( 𝜑 → 𝐴 = 𝐵 ) ∧ ( ¬ 𝜑 → 𝐴 = 𝐶 ) ) )
3	1 2	bitri	⊢ ( 𝐴 = if ( 𝜑 , 𝐵 , 𝐶 ) ↔ ( ( 𝜑 → 𝐴 = 𝐵 ) ∧ ( ¬ 𝜑 → 𝐴 = 𝐶 ) ) )