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 𝑅 → ( 𝑅 ∈ V ↔ ◡ 𝑅 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		cnvexg	⊢ ( 𝑅 ∈ V → ◡ 𝑅 ∈ V )
2		dfrel2	⊢ ( Rel 𝑅 ↔ ◡ ◡ 𝑅 = 𝑅 )
3		cnvexg	⊢ ( ◡ 𝑅 ∈ V → ◡ ◡ 𝑅 ∈ V )
4		eleq1	⊢ ( ◡ ◡ 𝑅 = 𝑅 → ( ◡ ◡ 𝑅 ∈ V ↔ 𝑅 ∈ V ) )
5	3 4	imbitrid	⊢ ( ◡ ◡ 𝑅 = 𝑅 → ( ◡ 𝑅 ∈ V → 𝑅 ∈ V ) )
6	2 5	sylbi	⊢ ( Rel 𝑅 → ( ◡ 𝑅 ∈ V → 𝑅 ∈ V ) )
7	1 6	impbid2	⊢ ( Rel 𝑅 → ( 𝑅 ∈ V ↔ ◡ 𝑅 ∈ V ) )