Metamath Proof Explorer

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 ⊢ R Er A → R ∈ V ↔ A ∈ V

Proof

Step Hyp Ref Expression
1 dmexg ⊢ R ∈ V → dom ⁡ R ∈ V
2 erdm ⊢ R Er A → dom ⁡ R = A
3 2 eleq1d ⊢ R Er A → dom ⁡ R ∈ V ↔ A ∈ V
4 1 3 imbitrid ⊢ R Er A → R ∈ V → A ∈ V
5 erex ⊢ R Er A → A ∈ V → R ∈ V
6 4 5 impbid ⊢ R Er A → R ∈ V ↔ A ∈ V