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

Theorem ifeq1 4443
 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 3459 . . 3 (𝐴 = 𝐵 → {𝑥𝐴𝜑} = {𝑥𝐵𝜑})
21uneq1d 4113 . 2 (𝐴 = 𝐵 → ({𝑥𝐴𝜑} ∪ {𝑥𝐶 ∣ ¬ 𝜑}) = ({𝑥𝐵𝜑} ∪ {𝑥𝐶 ∣ ¬ 𝜑}))
3 dfif6 4442 . 2 if(𝜑, 𝐴, 𝐶) = ({𝑥𝐴𝜑} ∪ {𝑥𝐶 ∣ ¬ 𝜑})
4 dfif6 4442 . 2 if(𝜑, 𝐵, 𝐶) = ({𝑥𝐵𝜑} ∪ {𝑥𝐶 ∣ ¬ 𝜑})
52, 3, 43eqtr4g 2882 1 (𝐴 = 𝐵 → if(𝜑, 𝐴, 𝐶) = if(𝜑, 𝐵, 𝐶))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538  {crab 3134   ∪ cun 3906  ifcif 4439 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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-12 2178  ax-ext 2794 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-rab 3139  df-v 3471  df-un 3913  df-if 4440 This theorem is referenced by:  ifeq12  4456  ifeq1d  4457  ifbieq12i  4465  rdgeq2  8035  dfoi  8963  wemaplem2  8999  cantnflem1  9140  prodeq2w  15257  prodeq2ii  15258  mgm2nsgrplem2  18075  mgm2nsgrplem3  18076  mplcoe3  20704  marrepval0  21164  ellimc  24474  ply1nzb  24721  dchrvmasumiflem1  26083  signspval  31896  dfrdg2  33114  dfafv22  43754
 Copyright terms: Public domain W3C validator