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	⊢ ( { 𝑋 } × 𝐶 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 = 𝑋 ∧ 𝑏 ∈ 𝐶 ) }

Proof

Step	Hyp	Ref	Expression
1		df-xp	⊢ ( { 𝑋 } × 𝐶 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ { 𝑋 } ∧ 𝑏 ∈ 𝐶 ) }
2		velsn	⊢ ( 𝑎 ∈ { 𝑋 } ↔ 𝑎 = 𝑋 )
3	2	anbi1i	⊢ ( ( 𝑎 ∈ { 𝑋 } ∧ 𝑏 ∈ 𝐶 ) ↔ ( 𝑎 = 𝑋 ∧ 𝑏 ∈ 𝐶 ) )
4	3	opabbii	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ { 𝑋 } ∧ 𝑏 ∈ 𝐶 ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 = 𝑋 ∧ 𝑏 ∈ 𝐶 ) }
5	1 4	eqtri	⊢ ( { 𝑋 } × 𝐶 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 = 𝑋 ∧ 𝑏 ∈ 𝐶 ) }