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

Theorem fvif 6859
Description: Move a conditional outside of a function. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
fvif (𝐹‘if(𝜑, 𝐴, 𝐵)) = if(𝜑, (𝐹𝐴), (𝐹𝐵))

Proof of Theorem fvif
StepHypRef Expression
1 fveq2 6843 . 2 (if(𝜑, 𝐴, 𝐵) = 𝐴 → (𝐹‘if(𝜑, 𝐴, 𝐵)) = (𝐹𝐴))
2 fveq2 6843 . 2 (if(𝜑, 𝐴, 𝐵) = 𝐵 → (𝐹‘if(𝜑, 𝐴, 𝐵)) = (𝐹𝐵))
31, 2ifsb 4500 1 (𝐹‘if(𝜑, 𝐴, 𝐵)) = if(𝜑, (𝐹𝐴), (𝐹𝐵))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  ifcif 4487  cfv 6497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505
This theorem is referenced by:  ccatco  14725  sumeq2ii  15579  prodeq2ii  15797  ruclem1  16114  xpsrnbas  17454  mat2pmat1  22084  decpmatid  22122  pmatcollpwscmatlem1  22141  copco  24384  pcopt  24388  pcopt2  24389  limccnp  25258  prmorcht  26530  pclogsum  26566  mblfinlem2  36119  ftc1anclem8  36161  ftc1anc  36162  rhmmpl  40744  fvifeq  45519
  Copyright terms: Public domain W3C validator