Metamath Proof Explorer

Theorem antisymrelressn

Description: (Contributed by Peter Mazsa, 29-Jun-2024)

Ref Expression
Assertion antisymrelressn 
|- AntisymRel ( R |` { A } )

Proof

Step Hyp Ref Expression
1 antisymressn 
 |-  A. x A. y ( ( x ( R |` { A } ) y /\ y ( R |` { A } ) x ) -> x = y )
2 relres 
 |-  Rel ( R |` { A } )
3 dfantisymrel5 
 |-  ( AntisymRel ( R |` { A } ) <-> ( A. x A. y ( ( x ( R |` { A } ) y /\ y ( R |` { A } ) x ) -> x = y ) /\ Rel ( R |` { A } ) ) )
4 1 2 3 mpbir2an 
 |-  AntisymRel ( R |` { A } )