Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-xp | Unicode 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, . Another example is that the set of rational numbers is defined using the Cartesian product as ; 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 | |
2 | cB | . . 3 | |
3 | 1, 2 | cxp 4596 | . 2 |
4 | vx | . . . . . 6 | |
5 | 4 | cv 1341 | . . . . 5 |
6 | 5, 1 | wcel 2135 | . . . 4 |
7 | vy | . . . . . 6 | |
8 | 7 | cv 1341 | . . . . 5 |
9 | 8, 2 | wcel 2135 | . . . 4 |
10 | 6, 9 | wa 103 | . . 3 |
11 | 10, 4, 7 | copab 4036 | . 2 |
12 | 3, 11 | wceq 1342 | 1 |
Colors of variables: wff set class |
This definition is referenced by: xpeq1 4612 xpeq2 4613 elxpi 4614 elxp 4615 nfxp 4625 fconstmpt 4645 brab2a 4651 xpundi 4654 xpundir 4655 opabssxp 4672 csbxpg 4679 xpss12 4705 inxp 4732 dmxpm 4818 dmxpid 4819 resopab 4922 cnvxp 5016 xpcom 5144 dfxp3 6154 dmaddpq 7311 dmmulpq 7312 enq0enq 7363 npsspw 7403 shftfvalg 10746 shftfval 10749 |
Copyright terms: Public domain | W3C validator |