Definition df-reflexive 46141

Description: Define reflexive relation; relation 𝑅 is reflexive over the set 𝐴 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 46140	. 2 wff 𝑅Reflexive𝐴
4	1, 1	cxp 5549	. . . 4 class (𝐴 × 𝐴)
5	2, 4	wss 3866	. . 3 wff 𝑅 ⊆ (𝐴 × 𝐴)
6		vx	. . . . . 6 setvar 𝑥
7	6	cv 1542	. . . . 5 class 𝑥
8	7, 7, 2	wbr 5053	. . . 4 wff 𝑥𝑅𝑥
9	8, 6, 1	wral 3061	. . 3 wff ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥
10	5, 9	wa 399	. 2 wff (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥)
11	3, 10	wb 209	1 wff (𝑅Reflexive𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥))

This definition is referenced by: (None)