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	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ dom ≀ 𝑅 ↔ ∃ 𝑢 𝑢 𝑅 𝐴 ) )