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 4609 | . 2 |
4 | vx | . . . . . 6 | |
5 | 4 | cv 1347 | . . . . 5 |
6 | 5, 1 | wcel 2141 | . . . 4 |
7 | vy | . . . . . 6 | |
8 | 7 | cv 1347 | . . . . 5 |
9 | 8, 2 | wcel 2141 | . . . 4 |
10 | 6, 9 | wa 103 | . . 3 |
11 | 10, 4, 7 | copab 4049 | . 2 |
12 | 3, 11 | wceq 1348 | 1 |
Colors of variables: wff set class |
This definition is referenced by: xpeq1 4625 xpeq2 4626 elxpi 4627 elxp 4628 nfxp 4638 fconstmpt 4658 brab2a 4664 xpundi 4667 xpundir 4668 opabssxp 4685 csbxpg 4692 xpss12 4718 inxp 4745 dmxpm 4831 dmxpid 4832 resopab 4935 cnvxp 5029 xpcom 5157 dfxp3 6173 dmaddpq 7341 dmmulpq 7342 enq0enq 7393 npsspw 7433 shftfvalg 10782 shftfval 10785 |
Copyright terms: Public domain | W3C validator |