Metamath Proof Explorer

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

Proof

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