Metamath Proof Explorer

Theorem elrels6

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

Ref Expression
Assertion elrels6 ⊢ R ∈ V → R ∈ Rels ↔ R ∩ dom ⁡ R × ran ⁡ R = R

Proof

Step Hyp Ref Expression
1 elrelsrel ⊢ R ∈ V → R ∈ Rels ↔ Rel ⁡ R
2 dfrel6 ⊢ Rel ⁡ R ↔ R ∩ dom ⁡ R × ran ⁡ R = R
3 1 2 syl6bb ⊢ R ∈ V → R ∈ Rels ↔ R ∩ dom ⁡ R × ran ⁡ R = R