Theorem ecex2

Description: Condition for a coset to be a set. (Contributed by Peter Mazsa, 4-May-2019)

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

Proof

Step	Hyp	Ref	Expression
1		ecexg	|- ( ( R |` A ) e. V -> [ B ] ( R |` A ) e. _V )
2		ecres2	|- ( B e. A -> [ B ] ( R |` A ) = [ B ] R )
3	2	eleq1d	|- ( B e. A -> ( [ B ] ( R |` A ) e. _V <-> [ B ] R e. _V ) )
4	1 3	syl5ibcom	|- ( ( R |` A ) e. V -> ( B e. A -> [ B ] R e. _V ) )