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 e. V /\ B e. W ) -> ( A e. [ B ] R <-> B R A ) )

Proof

Step Hyp Ref Expression
1 elimasng
 |-  ( ( B e. W /\ A e. V ) -> ( A e. ( R " { B } ) <-> <. B , A >. e. R ) )
2 1 ancoms
 |-  ( ( A e. V /\ B e. W ) -> ( A e. ( R " { B } ) <-> <. B , A >. e. R ) )
3 df-ec
 |-  [ B ] R = ( R " { B } )
4 3 eleq2i
 |-  ( A e. [ B ] R <-> A e. ( R " { B } ) )
5 df-br
 |-  ( B R A <-> <. B , A >. e. R )
6 2 4 5 3bitr4g
 |-  ( ( A e. V /\ B e. W ) -> ( A e. [ B ] R <-> B R A ) )