Theorem ecref

Description: All elements are in their own equivalence class. (Contributed by Thierry Arnoux, 14-Feb-2025)

	Ref	Expression
Assertion	ecref	⊢ ( ( 𝑅 Er 𝑋 ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ [ 𝐴 ] 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑅 Er 𝑋 ∧ 𝐴 ∈ 𝑋 ) → 𝑅 Er 𝑋 )
2		simpr	⊢ ( ( 𝑅 Er 𝑋 ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
3	1 2	erref	⊢ ( ( 𝑅 Er 𝑋 ∧ 𝐴 ∈ 𝑋 ) → 𝐴 𝑅 𝐴 )
4		elecg	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝐴 ) )
5	2 4	sylancom	⊢ ( ( 𝑅 Er 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝐴 ) )
6	3 5	mpbird	⊢ ( ( 𝑅 Er 𝑋 ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ [ 𝐴 ] 𝑅 )