Theorem ecref

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

	Ref	Expression
Assertion	ecref	|- ( ( R Er X /\ A e. X ) -> A e. [ A ] R )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( R Er X /\ A e. X ) -> R Er X )
2		simpr	|- ( ( R Er X /\ A e. X ) -> A e. X )
3	1 2	erref	|- ( ( R Er X /\ A e. X ) -> A R A )
4		elecg	|- ( ( A e. X /\ A e. X ) -> ( A e. [ A ] R <-> A R A ) )
5	2 4	sylancom	|- ( ( R Er X /\ A e. X ) -> ( A e. [ A ] R <-> A R A ) )
6	3 5	mpbird	|- ( ( R Er X /\ A e. X ) -> A e. [ A ] R )