Metamath Proof Explorer

Theorem elecALTV

Description: Elementhood in the R -coset of A . Theorem 72 of Suppes p. 82. (I think we should replace elecg with this original form of Suppes. Peter Mazsa). (Contributed by Mario Carneiro, 9-Jul-2014)

Ref Expression
Assertion elecALTV ⊢ A ∈ V ∧ B ∈ W → B ∈ A R ↔ A R B

Proof

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