This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-xp

Description: Define the Cartesian product of two classes. This is also sometimes called the "cross product" but that term also has other meanings; we intentionally choose a less ambiguous term. Definition 9.11 of Quine p. 64. For example, ( { 1 , 5 } X. { 2 , 7 } ) = ( { <. 1 , 2 >. , <. 1 , 7 >. } u. { <. 5 , 2 >. , <. 5 , 7 >. } ) ( ex-xp ). Another example is that the set of rational numbers is defined in df-q using the Cartesian product ( ZZ X. NN ) ; the left- and right-hand sides of the Cartesian product represent the top (integer) and bottom (natural) numbers of a fraction. (Contributed by NM, 4-Jul-1994)

		Ref	Expression
	Assertion	df-xp	⊢ ( 𝐴 × 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2	0 1	cxp	⊢ ( 𝐴 × 𝐵 )
3		vx	⊢ 𝑥
4		vy	⊢ 𝑦
5	3	cv	⊢ 𝑥
6	5 0	wcel	⊢ 𝑥 ∈ 𝐴
7	4	cv	⊢ 𝑦
8	7 1	wcel	⊢ 𝑦 ∈ 𝐵
9	6 8	wa	⊢ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 )
10	9 3 4	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) }
11	2 10	wceq	⊢ ( 𝐴 × 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) }