Definition df-reflexive 42509

Description: Define reflexive relation; relation R is reflexive over the set A iff A. x e. A x R x. (Contributed by David A. Wheeler, 1-Dec-2019.)

Assertion

Ref	Expression
df-reflexive	|- ( RReflexive A <-> ( R C_ ( A X. A ) /\ A. x e. A x R x ) )

Distinct variable groups:   x, A   x, R

Detailed syntax breakdown of Definition df-reflexive

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3	1, 2	wreflexive 42508	. 2 wff RReflexive A
4	1, 1	cxp 5112	. . . 4 class ( A X. A )
5	2, 4	wss 3574	. . 3 wff R C_ ( A X. A )
6		vx	. . . . . 6 setvar x
7	6	cv 1482	. . . . 5 class x
8	7, 7, 2	wbr 4653	. . . 4 wff x R x
9	8, 6, 1	wral 2912	. . 3 wff A. x e. A x R x
10	5, 9	wa 384	. 2 wff ( R C_ ( A X. A ) /\ A. x e. A x R x )
11	3, 10	wb 196	1 wff ( RReflexive A <-> ( R C_ ( A X. A ) /\ A. x e. A x R x ) )

This definition is referenced by: (None)