Mathbox for David A. Wheeler < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-reflexive Structured version   Visualization version   GIF version

Definition df-reflexive 45335
 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
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
31, 2wreflexive 45334 . 2 wff 𝑅Reflexive𝐴
41, 1cxp 5518 . . . 4 class (𝐴 × 𝐴)
52, 4wss 3881 . . 3 wff 𝑅 ⊆ (𝐴 × 𝐴)
6 vx . . . . . 6 setvar 𝑥
76cv 1537 . . . . 5 class 𝑥
87, 7, 2wbr 5031 . . . 4 wff 𝑥𝑅𝑥
98, 6, 1wral 3106 . . 3 wff 𝑥𝐴 𝑥𝑅𝑥
105, 9wa 399 . 2 wff (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥𝐴 𝑥𝑅𝑥)
113, 10wb 209 1 wff (𝑅Reflexive𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥𝐴 𝑥𝑅𝑥))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator