| Metamath Proof Explorer |
< Previous
Next >
Related theorems GIF version |
| Description: Extend the definition of a class to include the cross product. |
| Ref | Expression |
|---|---|
| cA | class A |
| cB | class B |
| Ref | Expression |
|---|---|
| cxp | class (A × B) |
| Colors of variables: wff set class |