Metamath Proof Explorer


Theorem cnvelrels

Description: The converse of a set is an element of the class of relations. (Contributed by Peter Mazsa, 18-Aug-2019)

Ref Expression
Assertion cnvelrels ( 𝐴𝑉 𝐴 ∈ Rels )

Proof

Step Hyp Ref Expression
1 relcnv Rel 𝐴
2 cnvexg ( 𝐴𝑉 𝐴 ∈ V )
3 elrelsrel ( 𝐴 ∈ V → ( 𝐴 ∈ Rels ↔ Rel 𝐴 ) )
4 2 3 syl ( 𝐴𝑉 → ( 𝐴 ∈ Rels ↔ Rel 𝐴 ) )
5 1 4 mpbiri ( 𝐴𝑉 𝐴 ∈ Rels )