This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database SUPPLEMENTARY MATERIAL (USERS' MATHBOXES) Mathbox for Peter Mazsa Relations 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 ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∈ Rels ↔ 𝑅 ⊆ ( V × V ) ) )
Proof
Step
Hyp
Ref
Expression
1
df-rels ⊢ Rels = 𝒫 ( V × V )
2
1
eleq2i ⊢ ( 𝑅 ∈ Rels ↔ 𝑅 ∈ 𝒫 ( V × V ) )
3
elpwg ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∈ 𝒫 ( V × V ) ↔ 𝑅 ⊆ ( V × V ) ) )
4
2 3
bitrid ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∈ Rels ↔ 𝑅 ⊆ ( V × V ) ) )