Theorem xpsnopab 48804

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

Assertion

Ref	Expression
xpsnopab	⊢ ({𝑋} × 𝐶) = {⟨𝑎, 𝑏⟩ ∣ (𝑎 = 𝑋 ∧ 𝑏 ∈ 𝐶)}

Distinct variable groups:   𝐶,𝑎,𝑏   𝑋,𝑎,𝑏

Proof of Theorem xpsnopab

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

Syntax hints:   ∧ wa 400   = wceq 1567   ∈ wcel 2149  {csn 4591  {copab 5174   × cxp 5657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-sn 4592  df-opab 5175  df-xp 5665

This theorem is referenced by:  xpiun  48805