Metamath Proof Explorer


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