Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Cosets by ` R `
eldmcoss
Next ⟩
eldmcoss2
Metamath Proof Explorer
Ascii
Unicode
Theorem
eldmcoss
Description:
Elementhood in the domain of cosets.
(Contributed by
Peter Mazsa
, 29-Mar-2019)
Ref
Expression
Assertion
eldmcoss
⊢
A
∈
V
→
A
∈
dom
⁡
≀
R
↔
∃
u
u
R
A
Proof
Step
Hyp
Ref
Expression
1
dmcoss3
⊢
dom
⁡
≀
R
=
dom
⁡
R
-1
2
1
eleq2i
⊢
A
∈
dom
⁡
≀
R
↔
A
∈
dom
⁡
R
-1
3
eldmcnv
⊢
A
∈
V
→
A
∈
dom
⁡
R
-1
↔
∃
u
u
R
A
4
2
3
syl5bb
⊢
A
∈
V
→
A
∈
dom
⁡
≀
R
↔
∃
u
u
R
A