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

Proof

Step	Hyp	Ref	Expression
1		brelrn.1	⊢ 𝐴 ∈ V
2		brelrn.2	⊢ 𝐵 ∈ V
3		brelrng	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 𝐶 𝐵 ) → 𝐵 ∈ ran 𝐶 )
4	1 2 3	mp3an12	⊢ ( 𝐴 𝐶 𝐵 → 𝐵 ∈ ran 𝐶 )