Metamath Proof Explorer


Theorem ecex2

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

Ref Expression
Assertion ecex2 R A V B A B R V

Proof

Step Hyp Ref Expression
1 ecexg R A V B R A V
2 ecres2 B A B R A = B R
3 2 eleq1d B A B R A V B R V
4 1 3 syl5ibcom R A V B A B R V