Description: Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | releldmb | ⊢ ( Rel 𝑅 → ( 𝐴 ∈ dom 𝑅 ↔ ∃ 𝑥 𝐴 𝑅 𝑥 ) ) |
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 𝑅 ↔ ∃ 𝑥 𝐴 𝑅 𝑥 ) ) |