![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-xp | Structured version Visualization version GIF version |
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} × {2, 7}) = ({〈1, 2〉, 〈1, 7〉} ∪ {〈5, 2〉, 〈5, 7〉}) (ex-xp 28005). Another example is that the set of rational numbers are defined in df-q 12161 using the Cartesian product (ℤ × ℕ); 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 |
---|---|
df-xp | ⊢ (𝐴 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | cxp 5401 | . 2 class (𝐴 × 𝐵) |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1506 | . . . . 5 class 𝑥 |
6 | 5, 1 | wcel 2050 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | vy | . . . . . 6 setvar 𝑦 | |
8 | 7 | cv 1506 | . . . . 5 class 𝑦 |
9 | 8, 2 | wcel 2050 | . . . 4 wff 𝑦 ∈ 𝐵 |
10 | 6, 9 | wa 387 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
11 | 10, 4, 7 | copab 4987 | . 2 class {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
12 | 3, 11 | wceq 1507 | 1 wff (𝐴 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
Colors of variables: wff setvar class |
This definition is referenced by: xpeq1 5417 xpss12 5418 xpeq2 5424 elxpi 5425 elxp 5426 nfxp 5436 fconstmpt 5460 xpundi 5466 xpundir 5467 opabssxp 5489 csbxp 5496 ssrel 5503 relopabiv 5539 relopabi 5540 inxp 5549 dmxp 5639 resopab 5744 cnvxp 5851 xpco 5975 1st2val 7527 2nd2val 7528 dfxp3 7565 marypha2lem2 8693 wemapwe 8952 cardf2 9164 dfac3 9339 axdc2lem 9666 fpwwe2lem1 9849 canthwe 9869 xpcogend 14193 shftfval 14288 ipoval 17634 ipolerval 17636 eqgfval 18123 frgpuplem 18670 ltbwe 19978 opsrtoslem1 19989 pjfval2 20567 2ndcctbss 21779 ulmval 24683 lgsquadlem3 25672 iscgrg 26012 ishpg 26259 nvss 28159 ajfval 28375 fpwrelmap 30242 afsval 31619 cvmlift2lem12 32175 dicval 37786 dnwech 39073 fgraphopab 39235 areaquad 39248 csbxpgVD 40676 relopabVD 40683 dfnelbr2 42903 xpsnopab 43425 |
Copyright terms: Public domain | W3C validator |