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\in V\to \left[A\right]R=\left\{y|ARy\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-ec	$$⊢\left[A\right]R=R\left[\left\{A\right\}\right]$$
2		imasng	$$⊢A\in V\to R\left[\left\{A\right\}\right]=\left\{y|ARy\right\}$$
3	1 2	eqtrid	$$⊢A\in V\to \left[A\right]R=\left\{y|ARy\right\}$$