Metamath Proof Explorer


Syntax definition wwe

Description: Extend wff notation to include the well-ordering predicate. Read: " R well-orders A ".

Ref Expression
Assertion wwe
wff R We A