Theorem xpsnopab

Description: A Cartesian product with a singleton expressed as ordered-pair class abstraction. (Contributed by AV, 27-Jan-2020)

	Ref	Expression
Assertion	xpsnopab	$$⊢\left\{X\right\}\times C=\left\{⟨a,b⟩|\left(a=X\wedge b\in C\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-xp	$$⊢\left\{X\right\}\times C=\left\{⟨a,b⟩|\left(a\in \left\{X\right\}\wedge b\in C\right)\right\}$$
2		velsn	$$⊢a\in \left\{X\right\}\leftrightarrow a=X$$
3	2	anbi1i	$$⊢\left(a\in \left\{X\right\}\wedge b\in C\right)\leftrightarrow \left(a=X\wedge b\in C\right)$$
4	3	opabbii	$$⊢\left\{⟨a,b⟩|\left(a\in \left\{X\right\}\wedge b\in C\right)\right\}=\left\{⟨a,b⟩|\left(a=X\wedge b\in C\right)\right\}$$
5	1 4	eqtri	$$⊢\left\{X\right\}\times C=\left\{⟨a,b⟩|\left(a=X\wedge b\in C\right)\right\}$$