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

Metamath Proof Explorer

Theorem elrels5

Description: Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021)

Ref Expression
Assertion elrels5 ⊢ R ∈ V → R ∈ Rels ↔ R ↾ dom ⁡ R = R

Proof

Step Hyp Ref Expression
1 elrelsrel ⊢ R ∈ V → R ∈ Rels ↔ Rel ⁡ R
2 dfrel5 ⊢ Rel ⁡ R ↔ R ↾ dom ⁡ R = R
3 1 2 bitrdi ⊢ R ∈ V → R ∈ Rels ↔ R ↾ dom ⁡ R = R