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

Theorem ifeq2 4063
 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 3179 . . 3 (𝐴 = 𝐵 → {𝑥𝐴 ∣ ¬ 𝜑} = {𝑥𝐵 ∣ ¬ 𝜑})
21uneq2d 3745 . 2 (𝐴 = 𝐵 → ({𝑥𝐶𝜑} ∪ {𝑥𝐴 ∣ ¬ 𝜑}) = ({𝑥𝐶𝜑} ∪ {𝑥𝐵 ∣ ¬ 𝜑}))
3 dfif6 4061 . 2 if(𝜑, 𝐶, 𝐴) = ({𝑥𝐶𝜑} ∪ {𝑥𝐴 ∣ ¬ 𝜑})
4 dfif6 4061 . 2 if(𝜑, 𝐶, 𝐵) = ({𝑥𝐶𝜑} ∪ {𝑥𝐵 ∣ ¬ 𝜑})
52, 3, 43eqtr4g 2680 1 (𝐴 = 𝐵 → if(𝜑, 𝐶, 𝐴) = if(𝜑, 𝐶, 𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1480  {crab 2911   ∪ cun 3553  ifcif 4058 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-v 3188  df-un 3560  df-if 4059 This theorem is referenced by:  ifeq12  4075  ifeq2d  4077  ifbieq2i  4082  ifexg  4129  somincom  5489  mdetunilem9  20345  prmorcht  24804  pclogsum  24840  matunitlindflem1  33034  ftc1anclem6  33119  ftc1anclem8  33121  ftc1anc  33122  hdmap1cbv  36569  hoidmv1le  40112  hoidmvlelem3  40115  vonn0ioo  40205  vonn0icc  40206
 Copyright terms: Public domain W3C validator