Theorem brdomain

Description: Binary relation form of the domain 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	brdomain	|- ( A Domain B <-> B = dom A )

Proof

Step	Hyp	Ref	Expression
1		brdomain.1	|- A e. _V
2		brdomain.2	|- B e. _V
3	1 2	brimage	|- ( A Image ( 1st |` ( _V X. _V ) ) B <-> B = ( ( 1st |` ( _V X. _V ) ) " A ) )
4		df-domain	|- Domain = Image ( 1st |` ( _V X. _V ) )
5	4	breqi	|- ( A Domain B <-> A Image ( 1st |` ( _V X. _V ) ) B )
6		dfdm5	|- dom A = ( ( 1st |` ( _V X. _V ) ) " A )
7	6	eqeq2i	|- ( B = dom A <-> B = ( ( 1st |` ( _V X. _V ) ) " A ) )
8	3 5 7	3bitr4i	|- ( A Domain B <-> B = dom A )