Theorem iffv

Description: Move a conditional outside of a function. (Contributed by Thierry Arnoux, 28-Sep-2018)

	Ref	Expression
Assertion	iffv	⊢ ( if ( 𝜑 , 𝐹 , 𝐺 ) ‘ 𝐴 ) = if ( 𝜑 , ( 𝐹 ‘ 𝐴 ) , ( 𝐺 ‘ 𝐴 ) )

Proof

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