Definition df-irreflexive

Description: Define irreflexive relation; relation R is irreflexive over the set A iff A. x e. A -. x R x . Note that a relation can be neither reflexive nor irreflexive. (Contributed by David A. Wheeler, 1-Dec-2019)

	Ref	Expression
Assertion	df-irreflexive	⊢ ( 𝑅 Irreflexive 𝐴 ↔ ( 𝑅 ⊆ ( 𝐴 × 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1		cA	⊢ 𝐴
2	1 0	wirreflexive	⊢ 𝑅 Irreflexive 𝐴
3	1 1	cxp	⊢ ( 𝐴 × 𝐴 )
4	0 3	wss	⊢ 𝑅 ⊆ ( 𝐴 × 𝐴 )
5		vx	⊢ 𝑥
6	5	cv	⊢ 𝑥
7	6 6 0	wbr	⊢ 𝑥 𝑅 𝑥
8	7	wn	⊢ ¬ 𝑥 𝑅 𝑥
9	8 5 1	wral	⊢ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥
10	4 9	wa	⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 )
11	2 10	wb	⊢ ( 𝑅 Irreflexive 𝐴 ↔ ( 𝑅 ⊆ ( 𝐴 × 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ) )