![]() |
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, ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-xp |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | 1, 2 | cxp 4624 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | vx |
. . . . . 6
![]() ![]() | |
5 | 4 | cv 1352 |
. . . . 5
![]() ![]() |
6 | 5, 1 | wcel 2148 |
. . . 4
![]() ![]() ![]() ![]() |
7 | vy |
. . . . . 6
![]() ![]() | |
8 | 7 | cv 1352 |
. . . . 5
![]() ![]() |
9 | 8, 2 | wcel 2148 |
. . . 4
![]() ![]() ![]() ![]() |
10 | 6, 9 | wa 104 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 10, 4, 7 | copab 4063 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 3, 11 | wceq 1353 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: xpeq1 4640 xpeq2 4641 elxpi 4642 elxp 4643 nfxp 4653 fconstmpt 4673 brab2a 4679 xpundi 4682 xpundir 4683 opabssxp 4700 csbxpg 4707 xpss12 4733 inxp 4761 dmxpm 4847 dmxpid 4848 resopab 4951 cnvxp 5047 xpcom 5175 dfxp3 6194 dmaddpq 7377 dmmulpq 7378 enq0enq 7429 npsspw 7469 shftfvalg 10826 shftfval 10829 eqgfval 13079 reldvdsrsrg 13259 dvdsrvald 13260 dvdsrex 13265 |
Copyright terms: Public domain | W3C validator |