HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Syntax Definition wer 4264
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 4267 for more information.
Colors of variables: wff set class
Copyright terms: Public domain