This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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