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 \to (R \in V \leftrightarrow A \in V)$

Proof

Step	Hyp	Ref	Expression
1		dmexg	$⊢ R \in V \to dom R \in V$
2		erdm	$⊢ R Er A \to dom R = A$
3	2	eleq1d	$⊢ R Er A \to (dom R \in V \leftrightarrow A \in V)$
4	1 3	imbitrid	$⊢ R Er A \to (R \in V \to A \in V)$
5		erex	$⊢ R Er A \to (A \in V \to R \in V)$
6	4 5	impbid	$⊢ R Er A \to (R \in V \leftrightarrow A \in V)$