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	⊢ ( 𝐴 ∈ 𝑉 → RefRel ( 𝑅 ↾ { 𝐴 } ) )

Proof

Step	Hyp	Ref	Expression
1		refressn	⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑥 ∈ ( dom ( 𝑅 ↾ { 𝐴 } ) ∩ ran ( 𝑅 ↾ { 𝐴 } ) ) 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑥 )
2		relres	⊢ Rel ( 𝑅 ↾ { 𝐴 } )
3		dfrefrel5	⊢ ( RefRel ( 𝑅 ↾ { 𝐴 } ) ↔ ( ∀ 𝑥 ∈ ( dom ( 𝑅 ↾ { 𝐴 } ) ∩ ran ( 𝑅 ↾ { 𝐴 } ) ) 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑥 ∧ Rel ( 𝑅 ↾ { 𝐴 } ) ) )
4	1 2 3	sylanblrc	⊢ ( 𝐴 ∈ 𝑉 → RefRel ( 𝑅 ↾ { 𝐴 } ) )