Theorem eldmcnv

Description: Elementhood in a domain of a converse. (Contributed by Peter Mazsa, 25-May-2018)

	Ref	Expression
Assertion	eldmcnv	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ dom ◡ 𝑅 ↔ ∃ 𝑢 𝑢 𝑅 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		eldmg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ dom ◡ 𝑅 ↔ ∃ 𝑢 𝐴 ◡ 𝑅 𝑢 ) )
2		brcnvg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑢 ∈ V ) → ( 𝐴 ◡ 𝑅 𝑢 ↔ 𝑢 𝑅 𝐴 ) )
3	2	elvd	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ◡ 𝑅 𝑢 ↔ 𝑢 𝑅 𝐴 ) )
4	3	exbidv	⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑢 𝐴 ◡ 𝑅 𝑢 ↔ ∃ 𝑢 𝑢 𝑅 𝐴 ) )
5	1 4	bitrd	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ dom ◡ 𝑅 ↔ ∃ 𝑢 𝑢 𝑅 𝐴 ) )