Metamath Proof Explorer

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 \land A \in X) \to A \in [A] R$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (R Er X \land A \in X) \to R Er X$
2		simpr	$⊢ (R Er X \land A \in X) \to A \in X$
3	1 2	erref	$⊢ (R Er X \land A \in X) \to A R A$
4		elecg	$⊢ (A \in X \land A \in X) \to (A \in [A] R \leftrightarrow A R A)$
5	2 4	sylancom	$⊢ (R Er X \land A \in X) \to (A \in [A] R \leftrightarrow A R A)$
6	3 5	mpbird	$⊢ (R Er X \land A \in X) \to A \in [A] R$