| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Define the cross product of two classes. Definition 9.11 of [Quine] p. 64. |
| Ref | Expression |
|---|---|
| df-xp |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA |
. . 3
| |
| 2 | cB |
. . 3
| |
| 3 | 1, 2 | cxp 3158 |
. 2
|
| 4 | vx |
. . . . . 6
| |
| 5 | 4 | cv 952 |
. . . . 5
|
| 6 | 5, 1 | wcel 955 |
. . . 4
|
| 7 | vy |
. . . . . 6
| |
| 8 | 7 | cv 952 |
. . . . 5
|
| 9 | 8, 2 | wcel 955 |
. . . 4
|
| 10 | 6, 9 | wa 223 |
. . 3
|
| 11 | 10, 4, 7 | copab 2656 |
. 2
|
| 12 | 3, 11 | wceq 953 |
1
|
| Colors of variables: wff set class |
| This definition is referenced by: xpeq1 3190 xpeq2 3191 elxp 3192 fconstopab 3200 xpundi 3215 xpundir 3216 opabssxp 3224 relopab 3256 dmxp 3321 resopab 3379 1st2val 4079 2nd2val 4080 aceq3 4705 genpdm 5077 infmap2lem2 7522 ajfval 8400 |