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

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

Proof of Theorem ifeq1
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 rabeq 3070 . . 3 (𝐴 = 𝐵 → {𝑥𝐴𝜑} = {𝑥𝐵𝜑})
21uneq1d 3632 . 2 (𝐴 = 𝐵 → ({𝑥𝐴𝜑} ∪ {𝑥𝐶 ∣ ¬ 𝜑}) = ({𝑥𝐵𝜑} ∪ {𝑥𝐶 ∣ ¬ 𝜑}))
3 dfif6 3942 . 2 if(𝜑, 𝐴, 𝐶) = ({𝑥𝐴𝜑} ∪ {𝑥𝐶 ∣ ¬ 𝜑})
4 dfif6 3942 . 2 if(𝜑, 𝐵, 𝐶) = ({𝑥𝐵𝜑} ∪ {𝑥𝐶 ∣ ¬ 𝜑})
52, 3, 43eqtr4g 2573 1 (𝐴 = 𝐵 → if(𝜑, 𝐴, 𝐶) = if(𝜑, 𝐵, 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1474  {crab 2804  cun 3442  ifcif 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-rab 2809  df-v 3079  df-un 3449  df-if 3940
This theorem is referenced by:  ifeq12  3956  ifeq1d  3957  ifbieq12i  3965  ifexg  4010  rdgeq2  7270  dfoi  8174  wemaplem2  8210  cantnflem1  8344  prodeq2w  14348  prodeq2ii  14349  mgm2nsgrplem2  17119  mgm2nsgrplem3  17120  mplcoe3  19189  marrepval0  20087  ellimc  23319  ply1nzb  23562  dchrvmasumiflem1  24880  signspval  29801  dfrdg2  30788  dfafv2  39756
  Copyright terms: Public domain W3C validator