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 | syl5eq | |- ( A e. V -> [ A ] R = { y | A R y } ) |