Users' Mathboxes 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 42274
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
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
31, 2wreflexive 42273 . 2 wff 𝑅Reflexive𝐴
41, 1cxp 5026 . . . 4 class (𝐴 × 𝐴)
52, 4wss 3539 . . 3 wff 𝑅 ⊆ (𝐴 × 𝐴)
6 vx . . . . . 6 setvar 𝑥
76cv 1473 . . . . 5 class 𝑥
87, 7, 2wbr 4577 . . . 4 wff 𝑥𝑅𝑥
98, 6, 1wral 2895 . . 3 wff 𝑥𝐴 𝑥𝑅𝑥
105, 9wa 382 . 2 wff (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥𝐴 𝑥𝑅𝑥)
113, 10wb 194 1 wff (𝑅Reflexive𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥𝐴 𝑥𝑅𝑥))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator