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 e. _V <-> A e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		dmexg	|- ( R e. _V -> dom R e. _V )
2		erdm	|- ( R Er A -> dom R = A )
3	2	eleq1d	|- ( R Er A -> ( dom R e. _V <-> A e. _V ) )
4	1 3	imbitrid	|- ( R Er A -> ( R e. _V -> A e. _V ) )
5		erex	|- ( R Er A -> ( A e. _V -> R e. _V ) )
6	4 5	impbid	|- ( R Er A -> ( R e. _V <-> A e. _V ) )