Metamath Proof Explorer


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 𝑅 ↔ ∃ 𝑥 𝐴 𝑅 𝑥 ) )