Metamath Proof Explorer


Theorem eldmcoss

Description: Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 29-Mar-2019)

Ref Expression
Assertion eldmcoss
|- ( A e. V -> ( A e. dom ,~ R <-> E. u u R A ) )

Proof

Step Hyp Ref Expression
1 dmcoss3
 |-  dom ,~ R = dom `' R
2 1 eleq2i
 |-  ( A e. dom ,~ R <-> A e. dom `' R )
3 eldmcnv
 |-  ( A e. V -> ( A e. dom `' R <-> E. u u R A ) )
4 2 3 syl5bb
 |-  ( A e. V -> ( A e. dom ,~ R <-> E. u u R A ) )