Theorem relelrnb

Description: Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015)

	Ref	Expression
Assertion	relelrnb	|- ( Rel R -> ( A e. ran R <-> E. x x R A ) )

Proof

Step	Hyp	Ref	Expression
1		elrng	|- ( A e. ran R -> ( A e. ran R <-> E. x x R A ) )
2	1	ibi	|- ( A e. ran R -> E. x x R A )
3		relelrn	|- ( ( Rel R /\ x R A ) -> A e. ran R )
4	3	ex	|- ( Rel R -> ( x R A -> A e. ran R ) )
5	4	exlimdv	|- ( Rel R -> ( E. x x R A -> A e. ran R ) )
6	2 5	impbid2	|- ( Rel R -> ( A e. ran R <-> E. x x R A ) )