Definition df-altxp

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2	0 1	caltxp	⊢ ( 𝐴 ×× 𝐵 )
3		vz	⊢ 𝑧
4		vx	⊢ 𝑥
5		vy	⊢ 𝑦
6	3	cv	⊢ 𝑧
7	4	cv	⊢ 𝑥
8	5	cv	⊢ 𝑦
9	7 8	caltop	⊢ ⟪ 𝑥 , 𝑦 ⟫
10	6 9	wceq	⊢ 𝑧 = ⟪ 𝑥 , 𝑦 ⟫
11	10 5 1	wrex	⊢ ∃ 𝑦 ∈ 𝐵 𝑧 = ⟪ 𝑥 , 𝑦 ⟫
12	11 4 0	wrex	⊢ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟪ 𝑥 , 𝑦 ⟫
13	12 3	cab	⊢ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ }
14	2 13	wceq	⊢ ( 𝐴 ×× 𝐵 ) = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ }