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 26685). Another example is that the set of rational numbers are defined in df-q 11665 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 5036 | . 2 class (𝐴 × 𝐵) |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1474 | . . . . 5 class 𝑥 |
6 | 5, 1 | wcel 1977 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | vy | . . . . . 6 setvar 𝑦 | |
8 | 7 | cv 1474 | . . . . 5 class 𝑦 |
9 | 8, 2 | wcel 1977 | . . . 4 wff 𝑦 ∈ 𝐵 |
10 | 6, 9 | wa 383 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
11 | 10, 4, 7 | copab 4642 | . 2 class {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
12 | 3, 11 | wceq 1475 | 1 wff (𝐴 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
Colors of variables: wff setvar class |
This definition is referenced by: xpeq1 5052 xpeq2 5053 elxpi 5054 elxp 5055 nfxp 5066 fconstmpt 5085 brab2a 5091 xpundi 5094 xpundir 5095 opabssxp 5116 csbxp 5123 ssrel 5130 xpss12 5148 relopabi 5167 inxp 5176 dmxp 5265 resopab 5366 cnvxp 5470 xpco 5592 1st2val 7085 2nd2val 7086 dfxp3 7119 marypha2lem2 8225 wemapwe 8477 cardf2 8652 dfac3 8827 axdc2lem 9153 fpwwe2lem1 9332 canthwe 9352 xpcogend 13561 shftfval 13658 ipoval 16977 ipolerval 16979 eqgfval 17465 frgpuplem 18008 ltbwe 19293 opsrtoslem1 19305 pjfval2 19872 2ndcctbss 21068 ulmval 23938 lgsquadlem3 24907 iscgrg 25207 ishpg 25451 iseupa 26492 nvss 26832 ajfval 27048 fpwrelmap 28896 afsval 30002 cvmlift2lem12 30550 dicval 35483 dnwech 36636 fgraphopab 36807 areaquad 36821 csbxpgOLD 38075 csbxpgVD 38152 relopabVD 38159 xpsnopab 41555 |
Copyright terms: Public domain | W3C validator |