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	|- A e. _V
	brdomain.2	|- B e. _V
Assertion	brrange	|- ( A Range B <-> B = ran A )

Proof

Step	Hyp	Ref	Expression
1		brdomain.1	|- A e. _V
2		brdomain.2	|- B e. _V
3	1 2	brimage	|- ( A Image ( 2nd |` ( _V X. _V ) ) B <-> B = ( ( 2nd |` ( _V X. _V ) ) " A ) )
4		df-range	|- Range = Image ( 2nd |` ( _V X. _V ) )
5	4	breqi	|- ( A Range B <-> A Image ( 2nd |` ( _V X. _V ) ) B )
6		dfrn5	|- ran A = ( ( 2nd |` ( _V X. _V ) ) " A )
7	6	eqeq2i	|- ( B = ran A <-> B = ( ( 2nd |` ( _V X. _V ) ) " A ) )
8	3 5 7	3bitr4i	|- ( A Range B <-> B = ran A )