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\in \mathrm{V}$$
	opco1i.2	$$⊢C\in \mathrm{V}$$
Assertion	opco1i	$$⊢B\left(F\circ 1^{st}\right)C=F\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		opco1i.1	$$⊢B\in \mathrm{V}$$
2		opco1i.2	$$⊢C\in \mathrm{V}$$
3	1	a1i	$$⊢\top \to B\in \mathrm{V}$$
4	2	a1i	$$⊢\top \to C\in \mathrm{V}$$
5	3 4	opco1	$$⊢\top \to B\left(F\circ 1^{st}\right)C=F\left(B\right)$$
6	5	mptru	$$⊢B\left(F\circ 1^{st}\right)C=F\left(B\right)$$