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 45337
 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 45336 . 2 wff 𝑅Irreflexive𝐴
41, 1cxp 5518 . . . 4 class (𝐴 × 𝐴)
52, 4wss 3881 . . 3 wff 𝑅 ⊆ (𝐴 × 𝐴)
6 vx . . . . . . 7 setvar 𝑥
76cv 1537 . . . . . 6 class 𝑥
87, 7, 2wbr 5031 . . . . 5 wff 𝑥𝑅𝑥
98wn 3 . . . 4 wff ¬ 𝑥𝑅𝑥
109, 6, 1wral 3106 . . 3 wff 𝑥𝐴 ¬ 𝑥𝑅𝑥
115, 10wa 399 . 2 wff (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥𝐴 ¬ 𝑥𝑅𝑥)
123, 11wb 209 1 wff (𝑅Irreflexive𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥𝐴 ¬ 𝑥𝑅𝑥))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator