Theorem ecexr

Description: A nonempty equivalence class implies the representative is a set. (Contributed by Mario Carneiro, 9-Jul-2014)

	Ref	Expression
Assertion	ecexr	|- ( A e. [ B ] R -> B e. _V )

Proof

Step	Hyp	Ref	Expression
1		n0i	|- ( A e. ( R " { B } ) -> -. ( R " { B } ) = (/) )
2		snprc	|- ( -. B e. _V <-> { B } = (/) )
3		imaeq2	|- ( { B } = (/) -> ( R " { B } ) = ( R " (/) ) )
4	2 3	sylbi	|- ( -. B e. _V -> ( R " { B } ) = ( R " (/) ) )
5		ima0	|- ( R " (/) ) = (/)
6	4 5	eqtrdi	|- ( -. B e. _V -> ( R " { B } ) = (/) )
7	1 6	nsyl2	|- ( A e. ( R " { B } ) -> B e. _V )
8		df-ec	|- [ B ] R = ( R " { B } )
9	7 8	eleq2s	|- ( A e. [ B ] R -> B e. _V )