This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐴 ↔ ( 𝑅 ⊆ ( 𝐴 × 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ) )