This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 ∈ 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 ) 𝐶 ) = ( 𝐹 ‘ 𝐵 )