wer - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF 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