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

Theorem ifeq2 4492
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 3422 . . 3 (𝐴 = 𝐵 → {𝑥𝐴 ∣ ¬ 𝜑} = {𝑥𝐵 ∣ ¬ 𝜑})
21uneq2d 4124 . 2 (𝐴 = 𝐵 → ({𝑥𝐶𝜑} ∪ {𝑥𝐴 ∣ ¬ 𝜑}) = ({𝑥𝐶𝜑} ∪ {𝑥𝐵 ∣ ¬ 𝜑}))
3 dfif6 4490 . 2 if(𝜑, 𝐶, 𝐴) = ({𝑥𝐶𝜑} ∪ {𝑥𝐴 ∣ ¬ 𝜑})
4 dfif6 4490 . 2 if(𝜑, 𝐶, 𝐵) = ({𝑥𝐶𝜑} ∪ {𝑥𝐵 ∣ ¬ 𝜑})
52, 3, 43eqtr4g 2802 1 (𝐴 = 𝐵 → if(𝜑, 𝐶, 𝐴) = if(𝜑, 𝐶, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  {crab 3408  cun 3909  ifcif 4487
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 2708
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 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-un 3916  df-if 4488
This theorem is referenced by:  ifeq12  4505  ifeq2d  4507  ifbieq2i  4512  somincom  6089  mdetunilem9  21972  prmorcht  26530  pclogsum  26566  matunitlindflem1  36077  ftc1anclem6  36159  ftc1anclem8  36161  ftc1anc  36162  hdmap1cbv  40268  reabssgn  41915  hoidmv1le  44842  hoidmvlelem3  44845  vonn0ioo  44935  vonn0icc  44936
  Copyright terms: Public domain W3C validator