Theorem brrange

Description: Binary relation form of the range function. (Contributed by Scott Fenton, 11-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Hypotheses	brdomain.1	⊢ 𝐴 ∈ V
	brdomain.2	⊢ 𝐵 ∈ V
Assertion	brrange	⊢ ( 𝐴 Range 𝐵 ↔ 𝐵 = ran 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		brdomain.1	⊢ 𝐴 ∈ V
2		brdomain.2	⊢ 𝐵 ∈ V
3	1 2	brimage	⊢ ( 𝐴 Image ( 2nd ↾ ( V × V ) ) 𝐵 ↔ 𝐵 = ( ( 2nd ↾ ( V × V ) ) “ 𝐴 ) )
4		df-range	⊢ Range = Image ( 2nd ↾ ( V × V ) )
5	4	breqi	⊢ ( 𝐴 Range 𝐵 ↔ 𝐴 Image ( 2nd ↾ ( V × V ) ) 𝐵 )
6		dfrn5	⊢ ran 𝐴 = ( ( 2nd ↾ ( V × V ) ) “ 𝐴 )
7	6	eqeq2i	⊢ ( 𝐵 = ran 𝐴 ↔ 𝐵 = ( ( 2nd ↾ ( V × V ) ) “ 𝐴 ) )
8	3 5 7	3bitr4i	⊢ ( 𝐴 Range 𝐵 ↔ 𝐵 = ran 𝐴 )