Metamath Proof Explorer

Theorem relcnvexb

Description: A relation is a set iff its converse is a set. (Contributed by FL, 3-Mar-2007)

Ref Expression
Assertion relcnvexb ⊢ Rel ⁡ R → R ∈ V ↔ R -1 ∈ V

Proof

Step Hyp Ref Expression
1 cnvexg ⊢ R ∈ V → R -1 ∈ V
2 dfrel2 ⊢ Rel ⁡ R ↔ R -1 -1 = R
3 cnvexg ⊢ R -1 ∈ V → R -1 -1 ∈ V
4 eleq1 ⊢ R -1 -1 = R → R -1 -1 ∈ V ↔ R ∈ V
5 3 4 syl5ib ⊢ R -1 -1 = R → R -1 ∈ V → R ∈ V
6 2 5 sylbi ⊢ Rel ⁡ R → R -1 ∈ V → R ∈ V
7 1 6 impbid2 ⊢ Rel ⁡ R → R ∈ V ↔ R -1 ∈ V