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

Theorem ifeq2 4534
Description: Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
Assertion
Ref Expression
ifeq2 (𝐴 = 𝐵 → if(𝜑, 𝐶, 𝐴) = if(𝜑, 𝐶, 𝐵))

Proof of Theorem ifeq2
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 rabeq 3447 . . 3 (𝐴 = 𝐵 → {𝑥𝐴 ∣ ¬ 𝜑} = {𝑥𝐵 ∣ ¬ 𝜑})
21uneq2d 4164 . 2 (𝐴 = 𝐵 → ({𝑥𝐶𝜑} ∪ {𝑥𝐴 ∣ ¬ 𝜑}) = ({𝑥𝐶𝜑} ∪ {𝑥𝐵 ∣ ¬ 𝜑}))
3 dfif6 4532 . 2 if(𝜑, 𝐶, 𝐴) = ({𝑥𝐶𝜑} ∪ {𝑥𝐴 ∣ ¬ 𝜑})
4 dfif6 4532 . 2 if(𝜑, 𝐶, 𝐵) = ({𝑥𝐶𝜑} ∪ {𝑥𝐵 ∣ ¬ 𝜑})
52, 3, 43eqtr4g 2798 1 (𝐴 = 𝐵 → if(𝜑, 𝐶, 𝐴) = if(𝜑, 𝐶, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  {crab 3433  cun 3947  ifcif 4529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-un 3954  df-if 4530
This theorem is referenced by:  ifeq12  4547  ifeq2d  4549  ifbieq2i  4554  somincom  6136  mdetunilem9  22122  prmorcht  26682  pclogsum  26718  matunitlindflem1  36484  ftc1anclem6  36566  ftc1anclem8  36568  ftc1anc  36569  hdmap1cbv  40673  reabssgn  42387  hoidmv1le  45310  hoidmvlelem3  45313  vonn0ioo  45403  vonn0icc  45404
  Copyright terms: Public domain W3C validator