This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elrnressn

Description: Element of the range of a restriction to a singleton. (Contributed by Peter Mazsa, 12-Jun-2024)

Ref Expression
Assertion elrnressn ⊢ A ∈ V ∧ B ∈ W → B ∈ ran ⁡ R ↾ A ↔ A R B

Proof

Step Hyp Ref Expression
1 elrnres ⊢ B ∈ W → B ∈ ran ⁡ R ↾ A ↔ ∃ x ∈ A x R B
2 breq1 ⊢ x = A → x R B ↔ A R B
3 2 rexsng ⊢ A ∈ V → ∃ x ∈ A x R B ↔ A R B
4 1 3 sylan9bbr ⊢ A ∈ V ∧ B ∈ W → B ∈ ran ⁡ R ↾ A ↔ A R B