| 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 4149 |
. 2
|
| 4 | vx |
. . . . . 6
| |
| 5 | 4 | cv 1614 |
. . . . 5
|
| 6 | 5, 1 | wcel 1617 |
. . . 4
|
| 7 | vy |
. . . . . 6
| |
| 8 | 7 | cv 1614 |
. . . . 5
|
| 9 | 8, 2 | wcel 1617 |
. . . 4
|
| 10 | 6, 9 | wa 433 |
. . 3
|
| 11 | 10, 4, 7 | copab 3597 |
. 2
|
| 12 | 3, 11 | wceq 1615 |
1
|
| Colors of variables: wff set class |
| This definition is referenced by: xpeq1 4181 xpeq2 4182 elxp 4183 hbxp 4191 csbxpg 4192 fconstopab 4198 xpundi 4215 xpundir 4216 opabssxp 4225 relopab 4266 inxp 4271 dmxp 4332 resopab 4405 cnvxp 4479 1st2val 5184 2nd2val 5185 hartogslem 5967 aceq3 6252 genpdm 6700 infmap2lem2 9379 ajfval 10832 inposet 15620 domncnt 15624 ranncnt 15625 filnetlem4 16728 filnet 16730 eroprf 16820 pcoloopf 17164 csbxpgVD 17813 |