Theorem fvif

Description: Move a conditional outside of a function. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	fvif	⊢ ( 𝐹 ‘ if ( 𝜑 , 𝐴 , 𝐵 ) ) = if ( 𝜑 , ( 𝐹 ‘ 𝐴 ) , ( 𝐹 ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 → ( 𝐹 ‘ if ( 𝜑 , 𝐴 , 𝐵 ) ) = ( 𝐹 ‘ 𝐴 ) )
2		fveq2	⊢ ( if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 → ( 𝐹 ‘ if ( 𝜑 , 𝐴 , 𝐵 ) ) = ( 𝐹 ‘ 𝐵 ) )
3	1 2	ifsb	⊢ ( 𝐹 ‘ if ( 𝜑 , 𝐴 , 𝐵 ) ) = if ( 𝜑 , ( 𝐹 ‘ 𝐴 ) , ( 𝐹 ‘ 𝐵 ) )