Description: Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 29-Mar-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | eldmcoss | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ dom ≀ 𝑅 ↔ ∃ 𝑢 𝑢 𝑅 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmcoss3 | ⊢ dom ≀ 𝑅 = dom ◡ 𝑅 | |
2 | 1 | eleq2i | ⊢ ( 𝐴 ∈ dom ≀ 𝑅 ↔ 𝐴 ∈ dom ◡ 𝑅 ) |
3 | eldmcnv | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ dom ◡ 𝑅 ↔ ∃ 𝑢 𝑢 𝑅 𝐴 ) ) | |
4 | 2 3 | syl5bb | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ dom ≀ 𝑅 ↔ ∃ 𝑢 𝑢 𝑅 𝐴 ) ) |