Definition df-altxp 31236

Description: Define Cartesian products of alternative ordered pairs. (Contributed by Scott Fenton, 23-Mar-2012.)

Assertion

Ref	Expression
df-altxp	⊢ (𝐴 ×× 𝐵) = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = ⟪𝑥, 𝑦⟫}

Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝑥,𝐵,𝑦,𝑧

Detailed syntax breakdown of Definition df-altxp

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	caltxp 31234	. 2 class (𝐴 ×× 𝐵)
4		vz	. . . . . . 7 setvar 𝑧
5	4	cv 1474	. . . . . 6 class 𝑧
6		vx	. . . . . . . 8 setvar 𝑥
7	6	cv 1474	. . . . . . 7 class 𝑥
8		vy	. . . . . . . 8 setvar 𝑦
9	8	cv 1474	. . . . . . 7 class 𝑦
10	7, 9	caltop 31233	. . . . . 6 class ⟪𝑥, 𝑦⟫
11	5, 10	wceq 1475	. . . . 5 wff 𝑧 = ⟪𝑥, 𝑦⟫
12	11, 8, 2	wrex 2897	. . . 4 wff ∃𝑦 ∈ 𝐵 𝑧 = ⟪𝑥, 𝑦⟫
13	12, 6, 1	wrex 2897	. . 3 wff ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = ⟪𝑥, 𝑦⟫
14	13, 4	cab 2596	. 2 class {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = ⟪𝑥, 𝑦⟫}
15	3, 14	wceq 1475	1 wff (𝐴 ×× 𝐵) = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = ⟪𝑥, 𝑦⟫}

This definition is referenced by:  altxpeq1  31250  altxpeq2  31251  elaltxp  31252