Theorem cosni

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

	Ref	Expression
Hypotheses	cosni.1	$$⊢B\in \mathrm{V}$$
	cosni.2	$$⊢C\in \mathrm{V}$$
Assertion	cosni	$$⊢A\circ \left\{⟨B,C⟩\right\}=\left\{B\right\}\times A\left[\left\{C\right\}\right]$$

Proof

Step	Hyp	Ref	Expression
1		cosni.1	$$⊢B\in \mathrm{V}$$
2		cosni.2	$$⊢C\in \mathrm{V}$$
3		cosn	$$⊢\left(B\in \mathrm{V}\wedge C\in \mathrm{V}\right)\to A\circ \left\{⟨B,C⟩\right\}=\left\{B\right\}\times A\left[\left\{C\right\}\right]$$
4	1 2 3	mp2an	$$⊢A\circ \left\{⟨B,C⟩\right\}=\left\{B\right\}\times A\left[\left\{C\right\}\right]$$