wreflexive - Mathbox for David A. Wheeler

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

Syntax Definition wreflexive 46140

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

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

**Assertion**
Ref	Expression
wreflexive	wff 𝑅Reflexive𝐴

See definition df-reflexive 46141 for more information.

Colors of variables: wff setvar class

W3C validator