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 𝐶 )