ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  iffalse GIF version

Theorem iffalse 3429
Description: Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.)
Assertion
Ref Expression
iffalse 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)

Proof of Theorem iffalse
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 dedlemb 922 . . 3 𝜑 → (𝑥𝐵 ↔ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))))
21abbi2dv 2218 . 2 𝜑𝐵 = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))})
3 df-if 3422 . 2 if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))}
42, 3syl6reqr 2151 1 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wo 670   = wceq 1299  wcel 1448  {cab 2086  ifcif 3421
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-11 1452  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082
This theorem depends on definitions:  df-bi 116  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-if 3422
This theorem is referenced by:  iffalsei  3430  iffalsed  3431  ifnefalse  3432  ifsbdc  3433  ifcldadc  3448  ifeq1dadc  3449  ifbothdadc  3450  ifbothdc  3451  ifiddc  3452  ifcldcd  3454  ifandc  3455  fidifsnen  6693  nnnninf  6935  uzin  9208  modifeq2int  10000  bcval  10336  bcval3  10338  sumrbdclem  10984  fsum3cvg  10985  summodclem2a  10989  sumsplitdc  11040  flodddiv4  11426  gcdn0val  11445  dfgcd2  11495  lcmn0val  11540
  Copyright terms: Public domain W3C validator