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