Metamath Proof Explorer

Theorem dfantisymrel5

Description: Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024)

Ref Expression
Assertion dfantisymrel5 
|- ( AntisymRel R <-> ( A. x A. y ( ( x R y /\ y R x ) -> x = y ) /\ Rel R ) )

Proof

Step Hyp Ref Expression
1 df-antisymrel 
 |-  ( AntisymRel R <-> ( CnvRefRel ( R i^i `' R ) /\ Rel R ) )
2 relcnv 
 |-  Rel `' R
3 relin2 
 |-  ( Rel `' R -> Rel ( R i^i `' R ) )
4 2 3 ax-mp 
 |-  Rel ( R i^i `' R )
5 dfcnvrefrel5 
 |-  ( CnvRefRel ( R i^i `' R ) <-> ( A. x A. y ( x ( R i^i `' R ) y -> x = y ) /\ Rel ( R i^i `' R ) ) )
6 4 5 mpbiran2 
 |-  ( CnvRefRel ( R i^i `' R ) <-> A. x A. y ( x ( R i^i `' R ) y -> x = y ) )
7 brcnvin 
 |-  ( ( x e. _V /\ y e. _V ) -> ( x ( R i^i `' R ) y <-> ( x R y /\ y R x ) ) )
8 7 el2v 
 |-  ( x ( R i^i `' R ) y <-> ( x R y /\ y R x ) )
9 8 imbi1i 
 |-  ( ( x ( R i^i `' R ) y -> x = y ) <-> ( ( x R y /\ y R x ) -> x = y ) )
10 9 2albii 
 |-  ( A. x A. y ( x ( R i^i `' R ) y -> x = y ) <-> A. x A. y ( ( x R y /\ y R x ) -> x = y ) )
11 6 10 bitri 
 |-  ( CnvRefRel ( R i^i `' R ) <-> A. x A. y ( ( x R y /\ y R x ) -> x = y ) )
12 1 11 bianbi 
 |-  ( AntisymRel R <-> ( A. x A. y ( ( x R y /\ y R x ) -> x = y ) /\ Rel R ) )