Theorem ercl

Description: Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Hypotheses	ersym.1	|- ( ph -> R Er X )
	ersym.2	|- ( ph -> A R B )
Assertion	ercl	|- ( ph -> A e. X )

Proof

Step	Hyp	Ref	Expression
1		ersym.1	|- ( ph -> R Er X )
2		ersym.2	|- ( ph -> A R B )
3		errel	|- ( R Er X -> Rel R )
4	1 3	syl	|- ( ph -> Rel R )
5		releldm	|- ( ( Rel R /\ A R B ) -> A e. dom R )
6	4 2 5	syl2anc	|- ( ph -> A e. dom R )
7		erdm	|- ( R Er X -> dom R = X )
8	1 7	syl	|- ( ph -> dom R = X )
9	6 8	eleqtrd	|- ( ph -> A e. X )