Theorem releldmb

Description: Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015)

	Ref	Expression
Assertion	releldmb	⊢ ( Rel 𝑅 → ( 𝐴 ∈ dom 𝑅 ↔ ∃ 𝑥 𝐴 𝑅 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		eldmg	⊢ ( 𝐴 ∈ dom 𝑅 → ( 𝐴 ∈ dom 𝑅 ↔ ∃ 𝑥 𝐴 𝑅 𝑥 ) )
2	1	ibi	⊢ ( 𝐴 ∈ dom 𝑅 → ∃ 𝑥 𝐴 𝑅 𝑥 )
3		releldm	⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝑥 ) → 𝐴 ∈ dom 𝑅 )
4	3	ex	⊢ ( Rel 𝑅 → ( 𝐴 𝑅 𝑥 → 𝐴 ∈ dom 𝑅 ) )
5	4	exlimdv	⊢ ( Rel 𝑅 → ( ∃ 𝑥 𝐴 𝑅 𝑥 → 𝐴 ∈ dom 𝑅 ) )
6	2 5	impbid2	⊢ ( Rel 𝑅 → ( 𝐴 ∈ dom 𝑅 ↔ ∃ 𝑥 𝐴 𝑅 𝑥 ) )