![]() |
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 } ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-xp |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | 1, 2 | cxp 4497 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | vx |
. . . . . 6
![]() ![]() | |
5 | 4 | cv 1313 |
. . . . 5
![]() ![]() |
6 | 5, 1 | wcel 1463 |
. . . 4
![]() ![]() ![]() ![]() |
7 | vy |
. . . . . 6
![]() ![]() | |
8 | 7 | cv 1313 |
. . . . 5
![]() ![]() |
9 | 8, 2 | wcel 1463 |
. . . 4
![]() ![]() ![]() ![]() |
10 | 6, 9 | wa 103 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 10, 4, 7 | copab 3948 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 3, 11 | wceq 1314 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: xpeq1 4513 xpeq2 4514 elxpi 4515 elxp 4516 nfxp 4526 fconstmpt 4546 brab2a 4552 xpundi 4555 xpundir 4556 opabssxp 4573 csbxpg 4580 xpss12 4606 inxp 4633 dmxpm 4719 dmxpid 4720 resopab 4821 cnvxp 4915 xpcom 5043 dfxp3 6046 dmaddpq 7135 dmmulpq 7136 enq0enq 7187 npsspw 7227 shftfvalg 10483 shftfval 10486 |
Copyright terms: Public domain | W3C validator |