Theorem brimage

Description: Binary relation form of the Image functor. (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Hypotheses	brimage.1	|- A e. _V
	brimage.2	|- B e. _V
Assertion	brimage	|- ( A Image R B <-> B = ( R " A ) )

Proof

Step	Hyp	Ref	Expression
1		brimage.1	|- A e. _V
2		brimage.2	|- B e. _V
3		df-image	|- Image R = ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E o. `' R ) (x) _V ) ) )
4		brxp	|- ( A ( _V X. _V ) B <-> ( A e. _V /\ B e. _V ) )
5	1 2 4	mpbir2an	|- A ( _V X. _V ) B
6		vex	|- x e. _V
7		vex	|- y e. _V
8	6 7	brcnv	|- ( x `' R y <-> y R x )
9	8	rexbii	|- ( E. y e. A x `' R y <-> E. y e. A y R x )
10	6 1	coep	|- ( x ( _E o. `' R ) A <-> E. y e. A x `' R y )
11	6	elima	|- ( x e. ( R " A ) <-> E. y e. A y R x )
12	9 10 11	3bitr4ri	|- ( x e. ( R " A ) <-> x ( _E o. `' R ) A )
13	1 2 3 5 12	brtxpsd3	|- ( A Image R B <-> B = ( R " A ) )