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

Theorem ifeq1 4311
 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 3389 . . 3 (𝐴 = 𝐵 → {𝑥𝐴𝜑} = {𝑥𝐵𝜑})
21uneq1d 3989 . 2 (𝐴 = 𝐵 → ({𝑥𝐴𝜑} ∪ {𝑥𝐶 ∣ ¬ 𝜑}) = ({𝑥𝐵𝜑} ∪ {𝑥𝐶 ∣ ¬ 𝜑}))
3 dfif6 4310 . 2 if(𝜑, 𝐴, 𝐶) = ({𝑥𝐴𝜑} ∪ {𝑥𝐶 ∣ ¬ 𝜑})
4 dfif6 4310 . 2 if(𝜑, 𝐵, 𝐶) = ({𝑥𝐵𝜑} ∪ {𝑥𝐶 ∣ ¬ 𝜑})
52, 3, 43eqtr4g 2839 1 (𝐴 = 𝐵 → if(𝜑, 𝐴, 𝐶) = if(𝜑, 𝐵, 𝐶))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1601  {crab 3094   ∪ cun 3790  ifcif 4307 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-un 3797  df-if 4308 This theorem is referenced by:  ifeq12  4324  ifeq1d  4325  ifbieq12i  4333  rdgeq2  7793  dfoi  8707  wemaplem2  8743  cantnflem1  8885  prodeq2w  15049  prodeq2ii  15050  mgm2nsgrplem2  17797  mgm2nsgrplem3  17798  mplcoe3  19867  marrepval0  20776  ellimc  24078  ply1nzb  24323  dchrvmasumiflem1  25646  signspval  31233  dfrdg2  32293  dfafv22  42310
 Copyright terms: Public domain W3C validator