Theorem opco1i

Description: Inference form of opco1 . (Contributed by Mario Carneiro, 28-May-2014) (Revised by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Hypotheses	opco1i.1	|- B e. _V
	opco1i.2	|- C e. _V
Assertion	opco1i	|- ( B ( F o. 1st ) C ) = ( F ` B )

Proof

Step	Hyp	Ref	Expression
1		opco1i.1	|- B e. _V
2		opco1i.2	|- C e. _V
3	1	a1i	|- ( T. -> B e. _V )
4	2	a1i	|- ( T. -> C e. _V )
5	3 4	opco1	|- ( T. -> ( B ( F o. 1st ) C ) = ( F ` B ) )
6	5	mptru	|- ( B ( F o. 1st ) C ) = ( F ` B )