Theorem trrelressn

Description: Any class ' R ' restricted to the singleton of the class ' A ' (see ressn2 ) is transitive. (Contributed by Peter Mazsa, 17-Jun-2024)

	Ref	Expression
Assertion	trrelressn	|- TrRel ( R |` { A } )

Proof

Step	Hyp	Ref	Expression
1		trressn	|- A. x A. y A. z ( ( x ( R |` { A } ) y /\ y ( R |` { A } ) z ) -> x ( R |` { A } ) z )
2		relres	|- Rel ( R |` { A } )
3		dftrrel3	|- ( TrRel ( R |` { A } ) <-> ( A. x A. y A. z ( ( x ( R |` { A } ) y /\ y ( R |` { A } ) z ) -> x ( R |` { A } ) z ) /\ Rel ( R |` { A } ) ) )
4	1 2 3	mpbir2an	|- TrRel ( R |` { A } )