Description: Extend wff definition to include "Reflexive" applied to a class, which is true iff class R is a reflexive relation over the set A. See df-reflexive . (Contributed by David A. Wheeler, 1-Dec-2019)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wreflexive | wff 𝑅 Reflexive 𝐴 |