![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-xp | GIF 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, ({1, 5} × {2, 7}) = ({〈1, 2〉, 〈1, 7〉} ∪ {〈5, 2〉, 〈5, 7〉}). 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 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | cxp 4621 | . 2 class (𝐴 × 𝐵) |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1352 | . . . . 5 class 𝑥 |
6 | 5, 1 | wcel 2148 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | vy | . . . . . 6 setvar 𝑦 | |
8 | 7 | cv 1352 | . . . . 5 class 𝑦 |
9 | 8, 2 | wcel 2148 | . . . 4 wff 𝑦 ∈ 𝐵 |
10 | 6, 9 | wa 104 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
11 | 10, 4, 7 | copab 4060 | . 2 class {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
12 | 3, 11 | wceq 1353 | 1 wff (𝐴 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
Colors of variables: wff set class |
This definition is referenced by: xpeq1 4637 xpeq2 4638 elxpi 4639 elxp 4640 nfxp 4650 fconstmpt 4670 brab2a 4676 xpundi 4679 xpundir 4680 opabssxp 4697 csbxpg 4704 xpss12 4730 inxp 4757 dmxpm 4843 dmxpid 4844 resopab 4947 cnvxp 5043 xpcom 5171 dfxp3 6189 dmaddpq 7366 dmmulpq 7367 enq0enq 7418 npsspw 7458 shftfvalg 10808 shftfval 10811 reldvdsrsrg 13083 dvdsrvald 13084 dvdsrex 13089 |
Copyright terms: Public domain | W3C validator |