Home
Metamath Proof Explorer
< Previous
Next >
Related theorems
Unicode version
Syntax Definition
wwe
2911
Description:
Extend wff notation to include the well-ordering predicate. Read: '
well-orders
.'
Hypotheses
Ref
Expression
cA
cR
Assertion
Ref
Expression
wwe
See definition
df-we
2929
for more information.
Colors of variables:
wff
set
class
Copyright terms:
Public domain