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 ⊢ 𝐴 ∈ V
brelrn.2 ⊢ 𝐵 ∈ V
Assertion opelrn ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 → 𝐵 ∈ ran 𝐶 )

Proof

Step Hyp Ref Expression
1 brelrn.1 ⊢ 𝐴 ∈ V
2 brelrn.2 ⊢ 𝐵 ∈ V
3 df-br ⊢ ( 𝐴 𝐶 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 )
4 1 2 brelrn ⊢ ( 𝐴 𝐶 𝐵 → 𝐵 ∈ ran 𝐶 )
5 3 4 sylbir ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 → 𝐵 ∈ ran 𝐶 )