This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-reflexive

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)

		Ref	Expression
	Assertion	df-reflexive	$⊢ R Reflexive A \leftrightarrow (R \subseteq A \times A \land \forall x \in A x R x)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$class R$
1		cA	$class A$
2	1 0	wreflexive	$wff R Reflexive A$
3	1 1	cxp	$class (A \times A)$
4	0 3	wss	$wff R \subseteq A \times A$
5		vx	$setvar x$
6	5	cv	$setvar x$
7	6 6 0	wbr	$wff x R x$
8	7 5 1	wral	$wff \forall x \in A x R x$
9	4 8	wa	$wff (R \subseteq A \times A \land \forall x \in A x R x)$
10	2 9	wb	$wff (R Reflexive A \leftrightarrow (R \subseteq A \times A \land \forall x \in A x R x))$