Description: Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | elrels5 | ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∈ Rels ↔ ( 𝑅 ↾ dom 𝑅 ) = 𝑅 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrelsrel | ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∈ Rels ↔ Rel 𝑅 ) ) | |
2 | dfrel5 | ⊢ ( Rel 𝑅 ↔ ( 𝑅 ↾ dom 𝑅 ) = 𝑅 ) | |
3 | 1 2 | bitrdi | ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∈ Rels ↔ ( 𝑅 ↾ dom 𝑅 ) = 𝑅 ) ) |