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

Theorem ifeq1 4227
 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 3341 . . 3 (𝐴 = 𝐵 → {𝑥𝐴𝜑} = {𝑥𝐵𝜑})
21uneq1d 3915 . 2 (𝐴 = 𝐵 → ({𝑥𝐴𝜑} ∪ {𝑥𝐶 ∣ ¬ 𝜑}) = ({𝑥𝐵𝜑} ∪ {𝑥𝐶 ∣ ¬ 𝜑}))
3 dfif6 4226 . 2 if(𝜑, 𝐴, 𝐶) = ({𝑥𝐴𝜑} ∪ {𝑥𝐶 ∣ ¬ 𝜑})
4 dfif6 4226 . 2 if(𝜑, 𝐵, 𝐶) = ({𝑥𝐵𝜑} ∪ {𝑥𝐶 ∣ ¬ 𝜑})
52, 3, 43eqtr4g 2829 1 (𝐴 = 𝐵 → if(𝜑, 𝐴, 𝐶) = if(𝜑, 𝐵, 𝐶))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1630  {crab 3064   ∪ cun 3719  ifcif 4223 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-rab 3069  df-v 3351  df-un 3726  df-if 4224 This theorem is referenced by:  ifeq12  4240  ifeq1d  4241  ifbieq12i  4249  ifexg  4294  rdgeq2  7660  dfoi  8571  wemaplem2  8607  cantnflem1  8749  prodeq2w  14848  prodeq2ii  14849  mgm2nsgrplem2  17613  mgm2nsgrplem3  17614  mplcoe3  19680  marrepval0  20584  ellimc  23856  ply1nzb  24101  dchrvmasumiflem1  25410  signspval  30963  dfrdg2  32031  dfafv2  41726
 Copyright terms: Public domain W3C validator