Theorem ercl

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

	Ref	Expression
Hypotheses	ersym.1	⊢ ( 𝜑 → 𝑅 Er 𝑋 )
	ersym.2	⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
Assertion	ercl	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		ersym.1	⊢ ( 𝜑 → 𝑅 Er 𝑋 )
2		ersym.2	⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
3		errel	⊢ ( 𝑅 Er 𝑋 → Rel 𝑅 )
4	1 3	syl	⊢ ( 𝜑 → Rel 𝑅 )
5		releldm	⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ∈ dom 𝑅 )
6	4 2 5	syl2anc	⊢ ( 𝜑 → 𝐴 ∈ dom 𝑅 )
7		erdm	⊢ ( 𝑅 Er 𝑋 → dom 𝑅 = 𝑋 )
8	1 7	syl	⊢ ( 𝜑 → dom 𝑅 = 𝑋 )
9	6 8	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )