Theorem fvifeq

Description: Equality of function values with conditional arguments, see also fvif . (Contributed by Alexander van der Vekens, 21-May-2018)

	Ref	Expression
Assertion	fvifeq	$$⊢A=if\left(\phi ,B,C\right)\to F\left(A\right)=if\left(\phi ,F\left(B\right),F\left(C\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢A=if\left(\phi ,B,C\right)\to F\left(A\right)=F\left(if\left(\phi ,B,C\right)\right)$$
2		fvif	$$⊢F\left(if\left(\phi ,B,C\right)\right)=if\left(\phi ,F\left(B\right),F\left(C\right)\right)$$
3	1 2	eqtrdi	$$⊢A=if\left(\phi ,B,C\right)\to F\left(A\right)=if\left(\phi ,F\left(B\right),F\left(C\right)\right)$$