Syntax Definition wirreflexive 42510

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 42511. (Contributed by David A. Wheeler, 1-Dec-2019.)

Hypotheses

Ref	Expression
cA	class A
cR	class R

Assertion

Ref	Expression
wirreflexive	wff RIrreflexive A

See definition df-irreflexive 42511 for more information.