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 44795
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 44794 . 2 wff 𝑅Reflexive𝐴
41, 1cxp 5546 . . . 4 class (𝐴 × 𝐴)
52, 4wss 3933 . . 3 wff 𝑅 ⊆ (𝐴 × 𝐴)
6 vx . . . . . 6 setvar 𝑥
76cv 1527 . . . . 5 class 𝑥
87, 7, 2wbr 5057 . . . 4 wff 𝑥𝑅𝑥
98, 6, 1wral 3135 . . 3 wff 𝑥𝐴 𝑥𝑅𝑥
105, 9wa 396 . 2 wff (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥𝐴 𝑥𝑅𝑥)
113, 10wb 207 1 wff (𝑅Reflexive𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥𝐴 𝑥𝑅𝑥))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator