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

Theorem eqif 4562
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 2736 . 2 (if(𝜑, 𝐵, 𝐶) = 𝐵 → (𝐴 = if(𝜑, 𝐵, 𝐶) ↔ 𝐴 = 𝐵))
2 eqeq2 2736 . 2 (if(𝜑, 𝐵, 𝐶) = 𝐶 → (𝐴 = if(𝜑, 𝐵, 𝐶) ↔ 𝐴 = 𝐶))
31, 2elimif 4558 1 (𝐴 = if(𝜑, 𝐵, 𝐶) ↔ ((𝜑𝐴 = 𝐵) ∨ (¬ 𝜑𝐴 = 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 395  wo 844   = wceq 1533  ifcif 4521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-if 4522
This theorem is referenced by:  ifval  4563  xpima  6172  fin23lem19  10328  fin23lem28  10332  fin23lem29  10333  fin23lem30  10334  aalioulem3  26190  ifnebib  32253  iocinif  32464  fsumcvg4  33422  ind1a  33509  esumsnf  33554  itg2addnclem2  37034  clsk1indlem4  43309  afvpcfv0  46364
  Copyright terms: Public domain W3C validator