Metamath Proof Explorer


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 V RefRel R A

Proof

Step Hyp Ref Expression
1 refressn A V x dom R A ran R A x R A x
2 relres Rel R A
3 dfrefrel5 RefRel R A x dom R A ran R A x R A x Rel R A
4 1 2 3 sylanblrc A V RefRel R A