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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | refressn | ||
2 | relres | ||
3 | dfrefrel5 | ||
4 | 1 2 3 | sylanblrc |