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 28143). Another example is that the set of rational numbers are defined in df-q 12338 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 5547 | . 2 class (𝐴 × 𝐵) |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1527 | . . . . 5 class 𝑥 |
6 | 5, 1 | wcel 2105 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | vy | . . . . . 6 setvar 𝑦 | |
8 | 7 | cv 1527 | . . . . 5 class 𝑦 |
9 | 8, 2 | wcel 2105 | . . . 4 wff 𝑦 ∈ 𝐵 |
10 | 6, 9 | wa 396 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
11 | 10, 4, 7 | copab 5120 | . 2 class {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
12 | 3, 11 | wceq 1528 | 1 wff (𝐴 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
Colors of variables: wff setvar class |
This definition is referenced by: xpeq1 5563 xpss12 5564 xpeq2 5570 elxpi 5571 elxp 5572 nfxp 5582 fconstmpt 5608 xpundi 5614 xpundir 5615 opabssxp 5637 csbxp 5644 ssrel 5651 relopabiv 5687 relopabi 5688 inxp 5697 dmxp 5793 resopab 5896 cnvxp 6008 xpco 6134 1st2val 7708 2nd2val 7709 dfxp3 7750 marypha2lem2 8889 wemapwe 9149 cardf2 9361 dfac3 9536 axdc2lem 9859 fpwwe2lem1 10042 canthwe 10062 xpcogend 14324 shftfval 14419 ipoval 17754 ipolerval 17756 eqgfval 18268 frgpuplem 18829 ltbwe 20183 opsrtoslem1 20194 pjfval2 20783 2ndcctbss 21993 ulmval 24897 lgsquadlem3 25886 iscgrg 26226 ishpg 26473 nvss 28298 ajfval 28514 fpwrelmap 30396 afsval 31842 cvmlift2lem12 32459 bj-opabssvv 34335 dicval 38194 dnwech 39528 fgraphopab 39690 areaquad 39703 csbxpgVD 41108 relopabVD 41115 dfnelbr2 43353 xpsnopab 43879 |
Copyright terms: Public domain | W3C validator |