Metamath Proof Explorer

Theorem relelrnb

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

Ref Expression
Assertion relelrnb ⊢ Rel ⁡ R → A ∈ ran ⁡ R ↔ ∃ x x R A

Proof

Step Hyp Ref Expression
1 elrng ⊢ A ∈ ran ⁡ R → A ∈ ran ⁡ R ↔ ∃ x x R A
2 1 ibi ⊢ A ∈ ran ⁡ R → ∃ x x R A
3 relelrn ⊢ Rel ⁡ R ∧ x R A → A ∈ ran ⁡ R
4 3 ex ⊢ Rel ⁡ R → x R A → A ∈ ran ⁡ R
5 4 exlimdv ⊢ Rel ⁡ R → ∃ x x R A → A ∈ ran ⁡ R
6 2 5 impbid2 ⊢ Rel ⁡ R → A ∈ ran ⁡ R ↔ ∃ x x R A