HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Syntax Definition wer 4258
Description: Extend the definition of a wff to include the equivalence predicate.
Hypothesis
Ref Expression
cR class R
Assertion
Ref Expression
wer wff Er R
See definition df-er 4261 for more information.
Colors of variables: wff set class
Copyright terms: Public domain