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	⊢ 𝐵 ∈ V
	opco1i.2	⊢ 𝐶 ∈ V
Assertion	opco1i	⊢ ( 𝐵 ( 𝐹 ∘ 1st ) 𝐶 ) = ( 𝐹 ‘ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		opco1i.1	⊢ 𝐵 ∈ V
2		opco1i.2	⊢ 𝐶 ∈ V
3	1	a1i	⊢ ( ⊤ → 𝐵 ∈ V )
4	2	a1i	⊢ ( ⊤ → 𝐶 ∈ V )
5	3 4	opco1	⊢ ( ⊤ → ( 𝐵 ( 𝐹 ∘ 1st ) 𝐶 ) = ( 𝐹 ‘ 𝐵 ) )
6	5	mptru	⊢ ( 𝐵 ( 𝐹 ∘ 1st ) 𝐶 ) = ( 𝐹 ‘ 𝐵 )