Theorem refrelressn

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

	Ref	Expression
Assertion	refrelressn	|- ( A e. V -> RefRel ( R |` { A } ) )

Proof

Step	Hyp	Ref	Expression
1		refressn	|- ( A e. V -> A. x e. ( dom ( R |` { A } ) i^i ran ( R |` { A } ) ) x ( R |` { A } ) x )
2		relres	|- Rel ( R |` { A } )
3		dfrefrel5	|- ( RefRel ( R |` { A } ) <-> ( A. x e. ( dom ( R |` { A } ) i^i ran ( R |` { A } ) ) x ( R |` { A } ) x /\ Rel ( R |` { A } ) ) )
4	1 2 3	sylanblrc	|- ( A e. V -> RefRel ( R |` { A } ) )