![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fvif | Structured version Visualization version GIF version |
Description: Move a conditional outside of a function. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Ref | Expression |
---|---|
fvif | ⊢ (𝐹‘if(𝜑, 𝐴, 𝐵)) = if(𝜑, (𝐹‘𝐴), (𝐹‘𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq2 6901 | . 2 ⊢ (if(𝜑, 𝐴, 𝐵) = 𝐴 → (𝐹‘if(𝜑, 𝐴, 𝐵)) = (𝐹‘𝐴)) | |
2 | fveq2 6901 | . 2 ⊢ (if(𝜑, 𝐴, 𝐵) = 𝐵 → (𝐹‘if(𝜑, 𝐴, 𝐵)) = (𝐹‘𝐵)) | |
3 | 1, 2 | ifsb 4546 | 1 ⊢ (𝐹‘if(𝜑, 𝐴, 𝐵)) = if(𝜑, (𝐹‘𝐴), (𝐹‘𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ifcif 4533 ‘cfv 6554 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-br 5154 df-iota 6506 df-fv 6562 |
This theorem is referenced by: ccatco 14844 sumeq2ii 15697 prodeq2ii 15915 ruclem1 16233 xpsrnbas 17586 rhmmpl 22374 rhmply1vr1 22378 mat2pmat1 22725 decpmatid 22763 pmatcollpwscmatlem1 22782 copco 25036 pcopt 25040 pcopt2 25041 limccnp 25911 prmorcht 27206 pclogsum 27244 mblfinlem2 37359 ftc1anclem8 37401 ftc1anc 37402 rhmpsr 42024 fvifeq 46893 |
Copyright terms: Public domain | W3C validator |