Theorem elrelimasn

Description: Elementhood in the image of a singleton. (Contributed by Mario Carneiro, 3-Nov-2015)

	Ref	Expression
Assertion	elrelimasn	|- ( Rel R -> ( B e. ( R " { A } ) <-> A R B ) )

Proof

Step	Hyp	Ref	Expression
1		relimasn	|- ( Rel R -> ( R " { A } ) = { x | A R x } )
2	1	eleq2d	|- ( Rel R -> ( B e. ( R " { A } ) <-> B e. { x | A R x } ) )
3		brrelex2	|- ( ( Rel R /\ A R B ) -> B e. _V )
4	3	ex	|- ( Rel R -> ( A R B -> B e. _V ) )
5		breq2	|- ( x = B -> ( A R x <-> A R B ) )
6	5	elab3g	|- ( ( A R B -> B e. _V ) -> ( B e. { x | A R x } <-> A R B ) )
7	4 6	syl	|- ( Rel R -> ( B e. { x | A R x } <-> A R B ) )
8	2 7	bitrd	|- ( Rel R -> ( B e. ( R " { A } ) <-> A R B ) )