Definition df-antisymrel

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

	Ref	Expression
Assertion	df-antisymrel	$$⊢AntisymRelR\leftrightarrow \left(CnvRefRel\left(R\cap R^{-1}\right)\wedge \mathrm{Rel}R\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1	0	wantisymrel	$$wffAntisymRelR$$
2	0	ccnv	$$class{R}^{-1}$$
3	0 2	cin	$$class\left(R\cap R^{-1}\right)$$
4	3	wcnvrefrel	$$wffCnvRefRel\left(R\cap R^{-1}\right)$$
5	0	wrel	$$wff\mathrm{Rel}R$$
6	4 5	wa	$$wff\left(CnvRefRel\left(R\cap R^{-1}\right)\wedge \mathrm{Rel}R\right)$$
7	1 6	wb	$$wff\left(AntisymRelR\leftrightarrow \left(CnvRefRel\left(R\cap R^{-1}\right)\wedge \mathrm{Rel}R\right)\right)$$