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

Metamath Proof Explorer

Theorem brelrn

Description: The second argument of a binary relation belongs to its range. (Contributed by NM, 13-Aug-2004)

Ref Expression
Hypotheses brelrn.1 ⊢ A ∈ V
brelrn.2 ⊢ B ∈ V
Assertion brelrn ⊢ A C B → B ∈ ran ⁡ C

Proof

Step Hyp Ref Expression
1 brelrn.1 ⊢ A ∈ V
2 brelrn.2 ⊢ B ∈ V
3 brelrng ⊢ A ∈ V ∧ B ∈ V ∧ A C B → B ∈ ran ⁡ C
4 1 2 3 mp3an12 ⊢ A C B → B ∈ ran ⁡ C