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

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | eqif | ⊢ ( 𝐴 = if ( 𝜑 , 𝐵 , 𝐶 ) ↔ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∨ ( ¬ 𝜑 ∧ 𝐴 = 𝐶 ) ) ) | |

2 | cases2 | ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∨ ( ¬ 𝜑 ∧ 𝐴 = 𝐶 ) ) ↔ ( ( 𝜑 → 𝐴 = 𝐵 ) ∧ ( ¬ 𝜑 → 𝐴 = 𝐶 ) ) ) | |

3 | 1 2 | bitri | ⊢ ( 𝐴 = if ( 𝜑 , 𝐵 , 𝐶 ) ↔ ( ( 𝜑 → 𝐴 = 𝐵 ) ∧ ( ¬ 𝜑 → 𝐴 = 𝐶 ) ) ) |