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	⊢ 𝐴 ∈ V
	brdomain.2	⊢ 𝐵 ∈ V
Assertion	brdomain	⊢ ( 𝐴 Domain 𝐵 ↔ 𝐵 = dom 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		brdomain.1	⊢ 𝐴 ∈ V
2		brdomain.2	⊢ 𝐵 ∈ V
3	1 2	brimage	⊢ ( 𝐴 Image ( 1st ↾ ( V × V ) ) 𝐵 ↔ 𝐵 = ( ( 1st ↾ ( V × V ) ) “ 𝐴 ) )
4		df-domain	⊢ Domain = Image ( 1st ↾ ( V × V ) )
5	4	breqi	⊢ ( 𝐴 Domain 𝐵 ↔ 𝐴 Image ( 1st ↾ ( V × V ) ) 𝐵 )
6		dfdm5	⊢ dom 𝐴 = ( ( 1st ↾ ( V × V ) ) “ 𝐴 )
7	6	eqeq2i	⊢ ( 𝐵 = dom 𝐴 ↔ 𝐵 = ( ( 1st ↾ ( V × V ) ) “ 𝐴 ) )
8	3 5 7	3bitr4i	⊢ ( 𝐴 Domain 𝐵 ↔ 𝐵 = dom 𝐴 )