relelec

Description: Membership in an equivalence class when R is a relation. (Contributed by Mario Carneiro, 11-Sep-2015)

		Ref	Expression
	Assertion	relelec	$⊢ Rel R \to (A \in [B] R \leftrightarrow B R A)$

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in [B] R \to A \in V$
2		ecexr	$⊢ A \in [B] R \to B \in V$
3	1 2	jca	$⊢ A \in [B] R \to (A \in V \land B \in V)$
4	3	adantl	$⊢ (Rel R \land A \in [B] R) \to (A \in V \land B \in V)$
5		brrelex12	$⊢ (Rel R \land B R A) \to (B \in V \land A \in V)$
6	5	ancomd	$⊢ (Rel R \land B R A) \to (A \in V \land B \in V)$
7		elecg	$⊢ (A \in V \land B \in V) \to (A \in [B] R \leftrightarrow B R A)$
8	4 6 7	pm5.21nd	$⊢ Rel R \to (A \in [B] R \leftrightarrow B R A)$

Metamath Proof Explorer