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	|- ( R Irreflexive A <-> ( R C_ ( A X. A ) /\ A. x e. A -. x R x ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	|- R
1		cA	|- A
2	1 0	wirreflexive	|- R Irreflexive A
3	1 1	cxp	|- ( A X. A )
4	0 3	wss	|- R C_ ( A X. A )
5		vx	|- x
6	5	cv	|- x
7	6 6 0	wbr	|- x R x
8	7	wn	|- -. x R x
9	8 5 1	wral	|- A. x e. A -. x R x
10	4 9	wa	|- ( R C_ ( A X. A ) /\ A. x e. A -. x R x )
11	2 10	wb	|- ( R Irreflexive A <-> ( R C_ ( A X. A ) /\ A. x e. A -. x R x ) )