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

Theorem ifeq2 4536
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 3448 . . 3 (𝐴 = 𝐵 → {𝑥𝐴 ∣ ¬ 𝜑} = {𝑥𝐵 ∣ ¬ 𝜑})
21uneq2d 4178 . 2 (𝐴 = 𝐵 → ({𝑥𝐶𝜑} ∪ {𝑥𝐴 ∣ ¬ 𝜑}) = ({𝑥𝐶𝜑} ∪ {𝑥𝐵 ∣ ¬ 𝜑}))
3 dfif6 4534 . 2 if(𝜑, 𝐶, 𝐴) = ({𝑥𝐶𝜑} ∪ {𝑥𝐴 ∣ ¬ 𝜑})
4 dfif6 4534 . 2 if(𝜑, 𝐶, 𝐵) = ({𝑥𝐶𝜑} ∪ {𝑥𝐵 ∣ ¬ 𝜑})
52, 3, 43eqtr4g 2800 1 (𝐴 = 𝐵 → if(𝜑, 𝐶, 𝐴) = if(𝜑, 𝐶, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1537  {crab 3433  cun 3961  ifcif 4531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-un 3968  df-if 4532
This theorem is referenced by:  ifeq12  4549  ifeq2d  4551  ifbieq2i  4556  somincom  6157  mdetunilem9  22642  prmorcht  27236  pclogsum  27274  matunitlindflem1  37603  ftc1anclem6  37685  ftc1anclem8  37687  ftc1anc  37688  hdmap1cbv  41785  reabssgn  43626  hoidmv1le  46550  hoidmvlelem3  46553  vonn0ioo  46643  vonn0icc  46644
  Copyright terms: Public domain W3C validator