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

Theorem ifeq2 4445
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 3460 . . 3 (𝐴 = 𝐵 → {𝑥𝐴 ∣ ¬ 𝜑} = {𝑥𝐵 ∣ ¬ 𝜑})
21uneq2d 4115 . 2 (𝐴 = 𝐵 → ({𝑥𝐶𝜑} ∪ {𝑥𝐴 ∣ ¬ 𝜑}) = ({𝑥𝐶𝜑} ∪ {𝑥𝐵 ∣ ¬ 𝜑}))
3 dfif6 4443 . 2 if(𝜑, 𝐶, 𝐴) = ({𝑥𝐶𝜑} ∪ {𝑥𝐴 ∣ ¬ 𝜑})
4 dfif6 4443 . 2 if(𝜑, 𝐶, 𝐵) = ({𝑥𝐶𝜑} ∪ {𝑥𝐵 ∣ ¬ 𝜑})
52, 3, 43eqtr4g 2881 1 (𝐴 = 𝐵 → if(𝜑, 𝐶, 𝐴) = if(𝜑, 𝐶, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1538  {crab 3130  cun 3908  ifcif 4440
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-rab 3135  df-v 3473  df-un 3915  df-if 4441
This theorem is referenced by:  ifeq12  4457  ifeq2d  4459  ifbieq2i  4464  somincom  5967  mdetunilem9  21204  prmorcht  25741  pclogsum  25777  noeta  33229  matunitlindflem1  34933  ftc1anclem6  35015  ftc1anclem8  35017  ftc1anc  35018  hdmap1cbv  38978  hoidmv1le  43026  hoidmvlelem3  43029  vonn0ioo  43119  vonn0icc  43120
  Copyright terms: Public domain W3C validator