| 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 30455). Another example is that the set of rational numbers is defined in df-q 12991 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 5683 | . 2 class (𝐴 × 𝐵) |
| 4 | vx | . . . . . 6 setvar 𝑥 | |
| 5 | 4 | cv 1539 | . . . . 5 class 𝑥 |
| 6 | 5, 1 | wcel 2108 | . . . 4 wff 𝑥 ∈ 𝐴 |
| 7 | vy | . . . . . 6 setvar 𝑦 | |
| 8 | 7 | cv 1539 | . . . . 5 class 𝑦 |
| 9 | 8, 2 | wcel 2108 | . . . 4 wff 𝑦 ∈ 𝐵 |
| 10 | 6, 9 | wa 395 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
| 11 | 10, 4, 7 | copab 5205 | . 2 class {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
| 12 | 3, 11 | wceq 1540 | 1 wff (𝐴 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
| Colors of variables: wff setvar class |
| This definition is referenced by: xpeq1 5699 xpss12 5700 xpeq2 5706 elxpi 5707 elxp 5708 nfxp 5718 fconstmpt 5747 xpundi 5754 xpundir 5755 elopaelxp 5775 opabssxp 5778 csbxp 5785 ssrel 5792 ssrelOLD 5793 relopabiv 5830 relopabi 5832 inxpOLD 5843 dmxpOLD 5940 resopab 6052 cnvxp 6177 xpco 6309 1st2val 8042 2nd2val 8043 dfxp3 8086 marypha2lem2 9476 wemapwe 9737 cardf2 9983 dfac3 10161 axdc2lem 10488 fpwwe2lem1 10671 canthwe 10691 xpcogend 15013 shftfval 15109 ipoval 18575 ipolerval 18577 eqgfval 19194 frgpuplem 19790 pjfval2 21729 ltbwe 22062 opsrtoslem1 22079 2ndcctbss 23463 ulmval 26423 lgsquadlem3 27426 iscgrg 28520 ishpg 28767 nvss 30612 ajfval 30828 fpwrelmap 32744 afsval 34686 cvmlift2lem12 35319 bj-opabssvv 37151 bj-xpcossxp 37190 dicval 41178 dnwech 43060 fgraphopab 43215 areaquad 43228 csbxpgVD 44914 relopabVD 44921 dfnelbr2 47285 xpsnopab 48073 |
| Copyright terms: Public domain | W3C validator |