Theorem elrn

Description: Membership in a range. (Contributed by NM, 2-Apr-2004)

	Ref	Expression
Hypothesis	elrn.1	|- A e. _V
Assertion	elrn	|- ( A e. ran B <-> E. x x B A )

Proof

Step	Hyp	Ref	Expression
1		elrn.1	|- A e. _V
2	1	elrn2	|- ( A e. ran B <-> E. x <. x , A >. e. B )
3		df-br	|- ( x B A <-> <. x , A >. e. B )
4	3	exbii	|- ( E. x x B A <-> E. x <. x , A >. e. B )
5	2 4	bitr4i	|- ( A e. ran B <-> E. x x B A )