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

Definition df-irreflexive 44797
Description: Define irreflexive relation; relation 𝑅 is irreflexive over the set 𝐴 iff 𝑥𝐴¬ 𝑥𝑅𝑥. Note that a relation can be neither reflexive nor irreflexive. (Contributed by David A. Wheeler, 1-Dec-2019.)
Assertion
Ref Expression
df-irreflexive (𝑅Irreflexive𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥𝐴 ¬ 𝑥𝑅𝑥))
Distinct variable groups:   𝑥,𝐴   𝑥,𝑅

Detailed syntax breakdown of Definition df-irreflexive
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
31, 2wirreflexive 44796 . 2 wff 𝑅Irreflexive𝐴
41, 1cxp 5546 . . . 4 class (𝐴 × 𝐴)
52, 4wss 3933 . . 3 wff 𝑅 ⊆ (𝐴 × 𝐴)
6 vx . . . . . . 7 setvar 𝑥
76cv 1527 . . . . . 6 class 𝑥
87, 7, 2wbr 5057 . . . . 5 wff 𝑥𝑅𝑥
98wn 3 . . . 4 wff ¬ 𝑥𝑅𝑥
109, 6, 1wral 3135 . . 3 wff 𝑥𝐴 ¬ 𝑥𝑅𝑥
115, 10wa 396 . 2 wff (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥𝐴 ¬ 𝑥𝑅𝑥)
123, 11wb 207 1 wff (𝑅Irreflexive𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥𝐴 ¬ 𝑥𝑅𝑥))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator