![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-xp | GIF 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 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | cxp 4369 | . 2 class (𝐴 × 𝐵) |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1284 | . . . . 5 class 𝑥 |
6 | 5, 1 | wcel 1434 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | vy | . . . . . 6 setvar 𝑦 | |
8 | 7 | cv 1284 | . . . . 5 class 𝑦 |
9 | 8, 2 | wcel 1434 | . . . 4 wff 𝑦 ∈ 𝐵 |
10 | 6, 9 | wa 102 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
11 | 10, 4, 7 | copab 3846 | . 2 class {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
12 | 3, 11 | wceq 1285 | 1 wff (𝐴 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
Colors of variables: wff set class |
This definition is referenced by: xpeq1 4385 xpeq2 4386 elxpi 4387 elxp 4388 nfxp 4397 fconstmpt 4413 brab2a 4419 xpundi 4422 xpundir 4423 opabssxp 4440 csbxpg 4447 xpss12 4473 inxp 4498 dmxpm 4583 resopab 4682 cnvxp 4772 xpcom 4894 dfxp3 5851 dmaddpq 6631 dmmulpq 6632 enq0enq 6683 npsspw 6723 shftfvalg 9844 shftfval 9847 |
Copyright terms: Public domain | W3C validator |