Definition df-reflexive 42318

Description: Define relexive relationship; relation R is reflexive over the set A iff ∀𝑥 ∈ 𝐴𝑥𝑅𝑥. (Contributed by David A. Wheeler, 1-Dec-2019.)

Assertion

Ref	Expression
df-reflexive	⊢ (𝑅Reflexive𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥))

Distinct variable groups:   𝑥,𝐴   𝑥,𝑅

Detailed syntax breakdown of Definition df-reflexive

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	wreflexive 42317	. 2 wff 𝑅Reflexive𝐴
4	1, 1	cxp 5036	. . . 4 class (𝐴 × 𝐴)
5	2, 4	wss 3540	. . 3 wff 𝑅 ⊆ (𝐴 × 𝐴)
6		vx	. . . . . 6 setvar 𝑥
7	6	cv 1474	. . . . 5 class 𝑥
8	7, 7, 2	wbr 4583	. . . 4 wff 𝑥𝑅𝑥
9	8, 6, 1	wral 2896	. . 3 wff ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥
10	5, 9	wa 383	. 2 wff (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥)
11	3, 10	wb 195	1 wff (𝑅Reflexive𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥))

This definition is referenced by: (None)