Theorem erexb

Description: An equivalence relation is a set if and only if its domain is a set. (Contributed by Rodolfo Medina, 15-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Assertion	erexb	⊢ ( 𝑅 Er 𝐴 → ( 𝑅 ∈ V ↔ 𝐴 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		dmexg	⊢ ( 𝑅 ∈ V → dom 𝑅 ∈ V )
2		erdm	⊢ ( 𝑅 Er 𝐴 → dom 𝑅 = 𝐴 )
3	2	eleq1d	⊢ ( 𝑅 Er 𝐴 → ( dom 𝑅 ∈ V ↔ 𝐴 ∈ V ) )
4	1 3	imbitrid	⊢ ( 𝑅 Er 𝐴 → ( 𝑅 ∈ V → 𝐴 ∈ V ) )
5		erex	⊢ ( 𝑅 Er 𝐴 → ( 𝐴 ∈ V → 𝑅 ∈ V ) )
6	4 5	impbid	⊢ ( 𝑅 Er 𝐴 → ( 𝑅 ∈ V ↔ 𝐴 ∈ V ) )