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 ) )