Metamath Proof Explorer

Theorem elrnres

Description: Element of the range of a restriction. (Contributed by Peter Mazsa, 26-Dec-2018)

Ref Expression
Assertion elrnres ⊢ B ∈ V → B ∈ ran ⁡ R ↾ A ↔ ∃ x ∈ A x R B

Proof

Step Hyp Ref Expression
1 elrng ⊢ B ∈ V → B ∈ ran ⁡ R ↾ A ↔ ∃ x x R ↾ A B
2 brres ⊢ B ∈ V → x R ↾ A B ↔ x ∈ A ∧ x R B
3 2 exbidv ⊢ B ∈ V → ∃ x x R ↾ A B ↔ ∃ x x ∈ A ∧ x R B
4 1 3 bitrd ⊢ B ∈ V → B ∈ ran ⁡ R ↾ A ↔ ∃ x x ∈ A ∧ x R B
5 df-rex ⊢ ∃ x ∈ A x R B ↔ ∃ x x ∈ A ∧ x R B
6 4 5 bitr4di ⊢ B ∈ V → B ∈ ran ⁡ R ↾ A ↔ ∃ x ∈ A x R B