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