| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Extend wff notation to
include the strict complete ordering predicate.
Read: ' |
| Ref | Expression |
|---|---|
| cA |
|
| cR |
|
| Ref | Expression |
|---|---|
| wor |
|
| Colors of variables: wff set class |