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 bitrid 
 |-  ( A e. V -> ( A e. dom ,~ R <-> E. u u R A ) )