Definition df-antisymrel 39300

Description: Define the antisymmetric relation predicate. (Read: 𝑅 is an antisymmetric relation.) (Contributed by Peter Mazsa, 24-Jun-2024.)

Assertion

Ref	Expression
df-antisymrel	⊢ ( AntisymRel 𝑅 ↔ ( CnvRefRel (𝑅 ∩ ◡𝑅) ∧ Rel 𝑅))

Detailed syntax breakdown of Definition df-antisymrel

Step	Hyp	Ref	Expression
1		cR	. . 3 class 𝑅
2	1	wantisymrel 38659	. 2 wff AntisymRel 𝑅
3	1	ccnv 5635	. . . . 5 class ◡𝑅
4	1, 3	cin 3894	. . . 4 class (𝑅 ∩ ◡𝑅)
5	4	wcnvrefrel 38629	. . 3 wff CnvRefRel (𝑅 ∩ ◡𝑅)
6	1	wrel 5641	. . 3 wff Rel 𝑅
7	5, 6	wa 398	. 2 wff ( CnvRefRel (𝑅 ∩ ◡𝑅) ∧ Rel 𝑅)
8	2, 7	wb 208	1 wff ( AntisymRel 𝑅 ↔ ( CnvRefRel (𝑅 ∩ ◡𝑅) ∧ Rel 𝑅))

This definition is referenced by:  dfantisymrel4  39301  dfantisymrel5  39302