Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-xp | Structured version Visualization version 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〉}) (ex-xp 28215). Another example is that the set of rational numbers are defined in df-q 12350 using the Cartesian product (ℤ × ℕ); 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 5553 | . 2 class (𝐴 × 𝐵) |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1536 | . . . . 5 class 𝑥 |
6 | 5, 1 | wcel 2114 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | vy | . . . . . 6 setvar 𝑦 | |
8 | 7 | cv 1536 | . . . . 5 class 𝑦 |
9 | 8, 2 | wcel 2114 | . . . 4 wff 𝑦 ∈ 𝐵 |
10 | 6, 9 | wa 398 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
11 | 10, 4, 7 | copab 5128 | . 2 class {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
12 | 3, 11 | wceq 1537 | 1 wff (𝐴 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
Colors of variables: wff setvar class |
This definition is referenced by: xpeq1 5569 xpss12 5570 xpeq2 5576 elxpi 5577 elxp 5578 nfxp 5588 fconstmpt 5614 xpundi 5620 xpundir 5621 opabssxp 5643 csbxp 5650 ssrel 5657 relopabiv 5693 relopabi 5694 inxp 5703 dmxp 5799 resopab 5902 cnvxp 6014 xpco 6140 1st2val 7717 2nd2val 7718 dfxp3 7759 marypha2lem2 8900 wemapwe 9160 cardf2 9372 dfac3 9547 axdc2lem 9870 fpwwe2lem1 10053 canthwe 10073 xpcogend 14334 shftfval 14429 ipoval 17764 ipolerval 17766 eqgfval 18328 frgpuplem 18898 ltbwe 20253 opsrtoslem1 20264 pjfval2 20853 2ndcctbss 22063 ulmval 24968 lgsquadlem3 25958 iscgrg 26298 ishpg 26545 nvss 28370 ajfval 28586 fpwrelmap 30469 afsval 31942 cvmlift2lem12 32561 bj-opabssvv 34445 dicval 38327 dnwech 39697 fgraphopab 39859 areaquad 39872 csbxpgVD 41277 relopabVD 41284 dfnelbr2 43521 xpsnopab 44081 |
Copyright terms: Public domain | W3C validator |