Theorem antisymrelressn

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

	Ref	Expression
Assertion	antisymrelressn	⊢ AntisymRel ( 𝑅 ↾ { 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		antisymressn	⊢ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 ∧ 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑥 ) → 𝑥 = 𝑦 )
2		relres	⊢ Rel ( 𝑅 ↾ { 𝐴 } )
3		dfantisymrel5	⊢ ( AntisymRel ( 𝑅 ↾ { 𝐴 } ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 ∧ 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ Rel ( 𝑅 ↾ { 𝐴 } ) ) )
4	1 2 3	mpbir2an	⊢ AntisymRel ( 𝑅 ↾ { 𝐴 } )