Theorem ereldm

Description: Equality of equivalence classes implies equivalence of domain membership. (Contributed by NM, 28-Jan-1996) (Revised by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Hypotheses	ereldm.1	|- ( ph -> R Er X )
	ereldm.2	|- ( ph -> [ A ] R = [ B ] R )
Assertion	ereldm	|- ( ph -> ( A e. X <-> B e. X ) )

Proof

Step	Hyp	Ref	Expression
1		ereldm.1	|- ( ph -> R Er X )
2		ereldm.2	|- ( ph -> [ A ] R = [ B ] R )
3	2	neeq1d	|- ( ph -> ( [ A ] R =/= (/) <-> [ B ] R =/= (/) ) )
4		ecdmn0	|- ( A e. dom R <-> [ A ] R =/= (/) )
5		ecdmn0	|- ( B e. dom R <-> [ B ] R =/= (/) )
6	3 4 5	3bitr4g	|- ( ph -> ( A e. dom R <-> B e. dom R ) )
7		erdm	|- ( R Er X -> dom R = X )
8	1 7	syl	|- ( ph -> dom R = X )
9	8	eleq2d	|- ( ph -> ( A e. dom R <-> A e. X ) )
10	8	eleq2d	|- ( ph -> ( B e. dom R <-> B e. X ) )
11	6 9 10	3bitr3d	|- ( ph -> ( A e. X <-> B e. X ) )