MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqif Structured version   Visualization version   GIF version

Theorem eqif 4566
Description: Expansion of an equality with a conditional operator. (Contributed by NM, 14-Feb-2005.)
Assertion
Ref Expression
eqif (𝐴 = if(𝜑, 𝐵, 𝐶) ↔ ((𝜑𝐴 = 𝐵) ∨ (¬ 𝜑𝐴 = 𝐶)))

Proof of Theorem eqif
StepHypRef Expression
1 eqeq2 2740 . 2 (if(𝜑, 𝐵, 𝐶) = 𝐵 → (𝐴 = if(𝜑, 𝐵, 𝐶) ↔ 𝐴 = 𝐵))
2 eqeq2 2740 . 2 (if(𝜑, 𝐵, 𝐶) = 𝐶 → (𝐴 = if(𝜑, 𝐵, 𝐶) ↔ 𝐴 = 𝐶))
31, 2elimif 4562 1 (𝐴 = if(𝜑, 𝐵, 𝐶) ↔ ((𝜑𝐴 = 𝐵) ∨ (¬ 𝜑𝐴 = 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 395  wo 846   = wceq 1534  ifcif 4525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-if 4526
This theorem is referenced by:  ifval  4567  xpima  6181  fin23lem19  10354  fin23lem28  10358  fin23lem29  10359  fin23lem30  10360  aalioulem3  26263  ifnebib  32334  iocinif  32544  fsumcvg4  33546  ind1a  33633  esumsnf  33678  itg2addnclem2  37140  clsk1indlem4  43465  afvpcfv0  46517
  Copyright terms: Public domain W3C validator