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

Metamath Proof Explorer

Theorem opelrn

Description: Membership of second member of an ordered pair in a range. (Contributed by NM, 23-Feb-1997)

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

Proof

Step Hyp Ref Expression
1 brelrn.1 ⊢ A ∈ V
2 brelrn.2 ⊢ B ∈ V
3 df-br ⊢ A C B ↔ A B ∈ C
4 1 2 brelrn ⊢ A C B → B ∈ ran ⁡ C
5 3 4 sylbir ⊢ A B ∈ C → B ∈ ran ⁡ C