Metamath Proof Explorer


Theorem eldmcoss

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

Ref Expression
Assertion eldmcoss ( 𝐴𝑉 → ( 𝐴 ∈ dom ≀ 𝑅 ↔ ∃ 𝑢 𝑢 𝑅 𝐴 ) )

Proof

Step Hyp Ref Expression
1 dmcoss3 dom ≀ 𝑅 = dom 𝑅
2 1 eleq2i ( 𝐴 ∈ dom ≀ 𝑅𝐴 ∈ dom 𝑅 )
3 eldmcnv ( 𝐴𝑉 → ( 𝐴 ∈ dom 𝑅 ↔ ∃ 𝑢 𝑢 𝑅 𝐴 ) )
4 2 3 syl5bb ( 𝐴𝑉 → ( 𝐴 ∈ dom ≀ 𝑅 ↔ ∃ 𝑢 𝑢 𝑅 𝐴 ) )