Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-xp | Unicode version |
Description: Define the cross product of two classes. Definition 9.11 of [Quine] p. 64. For example, ( { 1 , 5 } { 2 , 7 } ) = ( { 1 , 2 , 1 , 7 } { 5 , 2 , 5 , 7 } ) . Another example is that the set of rational numbers are defined in using the cross-product ( Z N ) ; the left- and right-hand sides of the cross-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 4507 | . 2 |
4 | vx | . . . . . 6 | |
5 | 4 | cv 1315 | . . . . 5 |
6 | 5, 1 | wcel 1465 | . . . 4 |
7 | vy | . . . . . 6 | |
8 | 7 | cv 1315 | . . . . 5 |
9 | 8, 2 | wcel 1465 | . . . 4 |
10 | 6, 9 | wa 103 | . . 3 |
11 | 10, 4, 7 | copab 3958 | . 2 |
12 | 3, 11 | wceq 1316 | 1 |
Colors of variables: wff set class |
This definition is referenced by: xpeq1 4523 xpeq2 4524 elxpi 4525 elxp 4526 nfxp 4536 fconstmpt 4556 brab2a 4562 xpundi 4565 xpundir 4566 opabssxp 4583 csbxpg 4590 xpss12 4616 inxp 4643 dmxpm 4729 dmxpid 4730 resopab 4833 cnvxp 4927 xpcom 5055 dfxp3 6060 dmaddpq 7155 dmmulpq 7156 enq0enq 7207 npsspw 7247 shftfvalg 10545 shftfval 10548 |
Copyright terms: Public domain | W3C validator |