Metamath Proof Explorer

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 ( ph , B , C ) -> ( F ` A ) = if ( ph , ( F ` B ) , ( F ` C ) ) )

Step	Hyp	Ref	Expression
1		fveq2	\|- ( A = if ( ph , B , C ) -> ( F ` A ) = ( F ` if ( ph , B , C ) ) )
2		fvif	\|- ( F ` if ( ph , B , C ) ) = if ( ph , ( F ` B ) , ( F ` C ) )
3	1 2	eqtrdi	\|- ( A = if ( ph , B , C ) -> ( F ` A ) = if ( ph , ( F ` B ) , ( F ` C ) ) )

Step

Hyp

Ref

Expression

 |-  ( A = if ( ph , B , C ) -> ( F ` A ) = ( F ` if ( ph , B , C ) ) )

 |-  ( F ` if ( ph , B , C ) ) = if ( ph , ( F ` B ) , ( F ` C ) )

1 2

 |-  ( A = if ( ph , B , C ) -> ( F ` A ) = if ( ph , ( F ` B ) , ( F ` C ) ) )