elecg

Description: Membership in an equivalence class. Theorem 72 of Suppes p. 82. (Contributed by Mario Carneiro, 9-Jul-2014)

		Ref	Expression
	Assertion	elecg	$⊢ (A \in V \land B \in W) \to (A \in [B] R \leftrightarrow B R A)$

Step	Hyp	Ref	Expression
1		elimasng	$⊢ (B \in W \land A \in V) \to (A \in R [\{B\}] \leftrightarrow ⟨B, A⟩ \in R)$
2	1	ancoms	$⊢ (A \in V \land B \in W) \to (A \in R [\{B\}] \leftrightarrow ⟨B, A⟩ \in R)$
3		df-ec	$⊢ [B] R = R [\{B\}]$
4	3	eleq2i	$⊢ A \in [B] R \leftrightarrow A \in R [\{B\}]$
5		df-br	$⊢ B R A \leftrightarrow ⟨B, A⟩ \in R$
6	2 4 5	3bitr4g	$⊢ (A \in V \land B \in W) \to (A \in [B] R \leftrightarrow B R A)$

Metamath Proof Explorer