Metamath Proof Explorer


Theorem dfec2

Description: Alternate definition of R -coset of A . Definition 34 of Suppes p. 81. (Contributed by NM, 3-Jan-1997) (Proof shortened by Mario Carneiro, 9-Jul-2014)

Ref Expression
Assertion dfec2
|- ( A e. V -> [ A ] R = { y | A R y } )

Proof

Step Hyp Ref Expression
1 df-ec
 |-  [ A ] R = ( R " { A } )
2 imasng
 |-  ( A e. V -> ( R " { A } ) = { y | A R y } )
3 1 2 eqtrid
 |-  ( A e. V -> [ A ] R = { y | A R y } )