Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Preparatory theorems
ecex2
Next ⟩
uniqsALTV
Metamath Proof Explorer
Ascii
Unicode
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