![]() |
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 30259). Another example is that the set of rational numbers is defined in df-q 12964 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 5676 | . 2 class (𝐴 × 𝐵) |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1533 | . . . . 5 class 𝑥 |
6 | 5, 1 | wcel 2099 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | vy | . . . . . 6 setvar 𝑦 | |
8 | 7 | cv 1533 | . . . . 5 class 𝑦 |
9 | 8, 2 | wcel 2099 | . . . 4 wff 𝑦 ∈ 𝐵 |
10 | 6, 9 | wa 395 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
11 | 10, 4, 7 | copab 5210 | . 2 class {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
12 | 3, 11 | wceq 1534 | 1 wff (𝐴 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
Colors of variables: wff setvar class |
This definition is referenced by: xpeq1 5692 xpss12 5693 xpeq2 5699 elxpi 5700 elxp 5701 nfxp 5711 fconstmpt 5740 xpundi 5746 xpundir 5747 elopaelxp 5767 opabssxp 5770 csbxp 5777 ssrel 5784 ssrelOLD 5785 relopabiv 5822 relopabi 5824 inxpOLD 5835 dmxp 5931 resopab 6038 cnvxp 6161 xpco 6293 1st2val 8021 2nd2val 8022 dfxp3 8065 marypha2lem2 9460 wemapwe 9721 cardf2 9967 dfac3 10145 axdc2lem 10472 fpwwe2lem1 10655 canthwe 10675 xpcogend 14954 shftfval 15050 ipoval 18522 ipolerval 18524 eqgfval 19131 frgpuplem 19727 pjfval2 21643 ltbwe 21982 opsrtoslem1 21999 2ndcctbss 23372 ulmval 26329 lgsquadlem3 27328 iscgrg 28329 ishpg 28576 nvss 30416 ajfval 30632 fpwrelmap 32528 afsval 34303 cvmlift2lem12 34924 bj-opabssvv 36629 bj-xpcossxp 36668 dicval 40649 dnwech 42472 fgraphopab 42631 areaquad 42644 csbxpgVD 44333 relopabVD 44340 dfnelbr2 46653 xpsnopab 47219 |
Copyright terms: Public domain | W3C validator |