Definition df-irreflexive 42511

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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	wirreflexive 42510	. 2 wff 𝑅Irreflexive𝐴
4	1, 1	cxp 5112	. . . 4 class (𝐴 × 𝐴)
5	2, 4	wss 3574	. . 3 wff 𝑅 ⊆ (𝐴 × 𝐴)
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1482	. . . . . 6 class 𝑥
8	7, 7, 2	wbr 4653	. . . . 5 wff 𝑥𝑅𝑥
9	8	wn 3	. . . 4 wff ¬ 𝑥𝑅𝑥
10	9, 6, 1	wral 2912	. . 3 wff ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥
11	5, 10	wa 384	. 2 wff (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥)
12	3, 11	wb 196	1 wff (𝑅Irreflexive𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥))

This definition is referenced by: (None)