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

Metamath Proof Explorer

Theorem elrels2

Description: The element of the relations class ( df-rels ) and the relation predicate ( df-rel ) are the same when R is a set. (Contributed by Peter Mazsa, 14-Jun-2018)

Ref Expression
Assertion elrels2 ⊢ R ∈ V → R ∈ Rels ↔ R ⊆ V × V

Proof

Step Hyp Ref Expression
1 df-rels ⊢ Rels = 𝒫 V × V
2 1 eleq2i ⊢ R ∈ Rels ↔ R ∈ 𝒫 V × V
3 elpwg ⊢ R ∈ V → R ∈ 𝒫 V × V ↔ R ⊆ V × V
4 2 3 bitrid ⊢ R ∈ V → R ∈ Rels ↔ R ⊆ V × V