Definition df-irreflexive

Description: Define irreflexive relation; relation R is irreflexive over the set A iff A. x e. A -. x R x . Note that a relation can be neither reflexive nor irreflexive. (Contributed by David A. Wheeler, 1-Dec-2019)

	Ref	Expression
Assertion	df-irreflexive	$$⊢RIrreflexiveA\leftrightarrow \left(R\subseteq A\times A\wedge \forall x\in A\neg xRx\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1		cA	$$classA$$
2	1 0	wirreflexive	$$wffRIrreflexiveA$$
3	1 1	cxp	$$class\left(A\times A\right)$$
4	0 3	wss	$$wffR\subseteq A\times A$$
5		vx	$$setvarx$$
6	5	cv	$$setvarx$$
7	6 6 0	wbr	$$wffxRx$$
8	7	wn	$$wff\neg xRx$$
9	8 5 1	wral	$$wff\forall x\in A\neg xRx$$
10	4 9	wa	$$wff\left(R\subseteq A\times A\wedge \forall x\in A\neg xRx\right)$$
11	2 10	wb	$$wff\left(RIrreflexiveA\leftrightarrow \left(R\subseteq A\times A\wedge \forall x\in A\neg xRx\right)\right)$$