wirreflexive - Mathbox for David A. Wheeler

	Mathbox for David A. Wheeler		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > wirreflexive		Structured version Visualization version GIF version

Syntax Definition wirreflexive 46142

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

**Hypotheses**
Ref	Expression
cA	class 𝐴
cR	class 𝑅

**Assertion**
Ref	Expression
wirreflexive	wff 𝑅Irreflexive𝐴

See definition df-irreflexive 46143 for more information.

Colors of variables: wff setvar class

W3C validator