Theorem cosn

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

	Ref	Expression
Assertion	cosn	⊢ ( ( 𝐵 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 ∘ { ⟨ 𝐵 , 𝐶 ⟩ } ) = ( { 𝐵 } × ( 𝐴 “ { 𝐶 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		xpsng	⊢ ( ( 𝐵 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) → ( { 𝐵 } × { 𝐶 } ) = { ⟨ 𝐵 , 𝐶 ⟩ } )
2	1	coeq2d	⊢ ( ( 𝐵 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 ∘ ( { 𝐵 } × { 𝐶 } ) ) = ( 𝐴 ∘ { ⟨ 𝐵 , 𝐶 ⟩ } ) )
3		coxp	⊢ ( 𝐴 ∘ ( { 𝐵 } × { 𝐶 } ) ) = ( { 𝐵 } × ( 𝐴 “ { 𝐶 } ) )
4	2 3	eqtr3di	⊢ ( ( 𝐵 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 ∘ { ⟨ 𝐵 , 𝐶 ⟩ } ) = ( { 𝐵 } × ( 𝐴 “ { 𝐶 } ) ) )