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	|- ( { X } X. C ) = { <. a , b >. | ( a = X /\ b e. C ) }

Proof

Step	Hyp	Ref	Expression
1		df-xp	|- ( { X } X. C ) = { <. a , b >. | ( a e. { X } /\ b e. C ) }
2		velsn	|- ( a e. { X } <-> a = X )
3	2	anbi1i	|- ( ( a e. { X } /\ b e. C ) <-> ( a = X /\ b e. C ) )
4	3	opabbii	|- { <. a , b >. | ( a e. { X } /\ b e. C ) } = { <. a , b >. | ( a = X /\ b e. C ) }
5	1 4	eqtri	|- ( { X } X. C ) = { <. a , b >. | ( a = X /\ b e. C ) }