Theorem cosn

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

	Ref	Expression
Assertion	cosn	$$⊢\left(B\in U\wedge C\in V\right)\to A\circ \left\{⟨B,C⟩\right\}=\left\{B\right\}\times A\left[\left\{C\right\}\right]$$

Proof

Step	Hyp	Ref	Expression
1		xpsng	$$⊢\left(B\in U\wedge C\in V\right)\to \left\{B\right\}\times \left\{C\right\}=\left\{⟨B,C⟩\right\}$$
2	1	coeq2d	$$⊢\left(B\in U\wedge C\in V\right)\to A\circ \left(\left\{B\right\}\times \left\{C\right\}\right)=A\circ \left\{⟨B,C⟩\right\}$$
3		coxp	$$⊢A\circ \left(\left\{B\right\}\times \left\{C\right\}\right)=\left\{B\right\}\times A\left[\left\{C\right\}\right]$$
4	2 3	eqtr3di	$$⊢\left(B\in U\wedge C\in V\right)\to A\circ \left\{⟨B,C⟩\right\}=\left\{B\right\}\times A\left[\left\{C\right\}\right]$$