Metamath Proof Explorer

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 
|- ( AntisymRel R <-> ( CnvRefRel ( R i^i `' R ) /\ Rel R ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR 
 |-  R
1 0 wantisymrel 
 |-  AntisymRel R
2 0 ccnv 
 |-  `' R
3 0 2 cin 
 |-  ( R i^i `' R )
4 3 wcnvrefrel 
 |-  CnvRefRel ( R i^i `' R )
5 0 wrel 
 |-  Rel R
6 4 5 wa 
 |-  ( CnvRefRel ( R i^i `' R ) /\ Rel R )
7 1 6 wb 
 |-  ( AntisymRel R <-> ( CnvRefRel ( R i^i `' R ) /\ Rel R ) )