![]() |
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 27423). Another example is that the set of rational numbers are defined in df-q 11827 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 5141 | . 2 class (𝐴 × 𝐵) |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1522 | . . . . 5 class 𝑥 |
6 | 5, 1 | wcel 2030 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | vy | . . . . . 6 setvar 𝑦 | |
8 | 7 | cv 1522 | . . . . 5 class 𝑦 |
9 | 8, 2 | wcel 2030 | . . . 4 wff 𝑦 ∈ 𝐵 |
10 | 6, 9 | wa 383 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
11 | 10, 4, 7 | copab 4745 | . 2 class {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
12 | 3, 11 | wceq 1523 | 1 wff (𝐴 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
Colors of variables: wff setvar class |
This definition is referenced by: xpeq1 5157 xpss12 5158 xpeq2 5163 elxpi 5164 elxp 5165 nfxp 5176 fconstmpt 5197 xpundi 5205 xpundir 5206 opabssxp 5227 csbxp 5234 ssrel 5241 relopabi 5278 inxp 5287 dmxp 5376 resopab 5481 cnvxp 5586 xpco 5713 1st2val 7238 2nd2val 7239 dfxp3 7275 marypha2lem2 8383 wemapwe 8632 cardf2 8807 dfac3 8982 axdc2lem 9308 fpwwe2lem1 9491 canthwe 9511 xpcogend 13759 shftfval 13854 ipoval 17201 ipolerval 17203 eqgfval 17689 frgpuplem 18231 ltbwe 19520 opsrtoslem1 19532 pjfval2 20101 2ndcctbss 21306 ulmval 24179 lgsquadlem3 25152 iscgrg 25452 ishpg 25696 nvss 27576 ajfval 27792 fpwrelmap 29636 afsval 30877 cvmlift2lem12 31422 dicval 36782 dnwech 37935 fgraphopab 38105 areaquad 38119 csbxpgOLD 39368 csbxpgVD 39444 relopabVD 39451 dfnelbr2 41614 xpsnopab 42090 |
Copyright terms: Public domain | W3C validator |