Theorem cosni

Description: Composition with an ordered pair singleton. (Contributed by Zhi Wang, 6-Oct-2025)

	Ref	Expression
Hypotheses	cosni.1	⊢ 𝐵 ∈ V
	cosni.2	⊢ 𝐶 ∈ V
Assertion	cosni	⊢ ( 𝐴 ∘ { ⟨ 𝐵 , 𝐶 ⟩ } ) = ( { 𝐵 } × ( 𝐴 “ { 𝐶 } ) )

Proof

Step	Hyp	Ref	Expression
1		cosni.1	⊢ 𝐵 ∈ V
2		cosni.2	⊢ 𝐶 ∈ V
3		cosn	⊢ ( ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( 𝐴 ∘ { ⟨ 𝐵 , 𝐶 ⟩ } ) = ( { 𝐵 } × ( 𝐴 “ { 𝐶 } ) ) )
4	1 2 3	mp2an	⊢ ( 𝐴 ∘ { ⟨ 𝐵 , 𝐶 ⟩ } ) = ( { 𝐵 } × ( 𝐴 “ { 𝐶 } ) )