Metamath Proof Explorer

Theorem 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 ∈ V ∧ B ∈ W → A ∈ B R ↔ B R A

Proof

Step Hyp Ref Expression
1 elimasng ⊢ B ∈ W ∧ A ∈ V → A ∈ R B ↔ B A ∈ R
2 1 ancoms ⊢ A ∈ V ∧ B ∈ W → A ∈ R B ↔ B A ∈ R
3 df-ec ⊢ B R = R B
4 3 eleq2i ⊢ A ∈ B R ↔ A ∈ R B
5 df-br ⊢ B R A ↔ B A ∈ R
6 2 4 5 3bitr4g ⊢ A ∈ V ∧ B ∈ W → A ∈ B R ↔ B R A