Metamath Proof Explorer

Theorem relelrn

Description: The second argument of a binary relation belongs to its range. (Contributed by NM, 2-Jul-2008)

Ref Expression
Assertion relelrn ⊢ Rel ⁡ R ∧ A R B → B ∈ ran ⁡ R

Proof

Step Hyp Ref Expression
1 brrelex1 ⊢ Rel ⁡ R ∧ A R B → A ∈ V
2 brrelex2 ⊢ Rel ⁡ R ∧ A R B → B ∈ V
3 simpr ⊢ Rel ⁡ R ∧ A R B → A R B
4 brelrng ⊢ A ∈ V ∧ B ∈ V ∧ A R B → B ∈ ran ⁡ R
5 1 2 3 4 syl3anc ⊢ Rel ⁡ R ∧ A R B → B ∈ ran ⁡ R