Theorem ecex2

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

	Ref	Expression
Assertion	ecex2	$$⊢{R\upharpoonright }_A\in V\to \left(B\in A\to \left[B\right]R\in \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ecexg	$$⊢{R\upharpoonright }_A\in V\to \left[B\right]\left({R\upharpoonright }_A\right)\in \mathrm{V}$$
2		ecres2	$$⊢B\in A\to \left[B\right]\left({R\upharpoonright }_A\right)=\left[B\right]R$$
3	2	eleq1d	$$⊢B\in A\to \left(\left[B\right]\left({R\upharpoonright }_A\right)\in \mathrm{V}\leftrightarrow \left[B\right]R\in \mathrm{V}\right)$$
4	1 3	syl5ibcom	$$⊢{R\upharpoonright }_A\in V\to \left(B\in A\to \left[B\right]R\in \mathrm{V}\right)$$