![]() |
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 28221). Another example is that the set of rational numbers are defined in df-q 12337 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 5517 | . 2 class (𝐴 × 𝐵) |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1537 | . . . . 5 class 𝑥 |
6 | 5, 1 | wcel 2111 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | vy | . . . . . 6 setvar 𝑦 | |
8 | 7 | cv 1537 | . . . . 5 class 𝑦 |
9 | 8, 2 | wcel 2111 | . . . 4 wff 𝑦 ∈ 𝐵 |
10 | 6, 9 | wa 399 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
11 | 10, 4, 7 | copab 5092 | . 2 class {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
12 | 3, 11 | wceq 1538 | 1 wff (𝐴 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
Colors of variables: wff setvar class |
This definition is referenced by: xpeq1 5533 xpss12 5534 xpeq2 5540 elxpi 5541 elxp 5542 nfxp 5552 fconstmpt 5578 xpundi 5584 xpundir 5585 opabssxp 5607 csbxp 5614 ssrel 5621 relopabiv 5657 relopabi 5658 inxp 5667 dmxp 5763 resopab 5869 cnvxp 5981 xpco 6108 1st2val 7699 2nd2val 7700 dfxp3 7741 marypha2lem2 8884 wemapwe 9144 cardf2 9356 dfac3 9532 axdc2lem 9859 fpwwe2lem1 10042 canthwe 10062 xpcogend 14325 shftfval 14421 ipoval 17756 ipolerval 17758 eqgfval 18320 frgpuplem 18890 pjfval2 20398 ltbwe 20712 opsrtoslem1 20723 2ndcctbss 22060 ulmval 24975 lgsquadlem3 25966 iscgrg 26306 ishpg 26553 nvss 28376 ajfval 28592 fpwrelmap 30495 afsval 32052 cvmlift2lem12 32674 bj-opabssvv 34565 bj-xpcossxp 34604 dicval 38472 dnwech 39992 fgraphopab 40154 areaquad 40166 csbxpgVD 41600 relopabVD 41607 dfnelbr2 43829 xpsnopab 44385 |
Copyright terms: Public domain | W3C validator |