| Metamath Proof Explorer |
< Previous
Next >
Related theorems GIF version |
| Description: Extend wff notation to include the well-ordering predicate. Read: 'R well-orders A.' |
| Ref | Expression |
|---|---|
| cA | class A |
| cR | class R |
| Ref | Expression |
|---|---|
| wwe | wff R We A |
| Colors of variables: wff set class |