Theorem elrng

Description: Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011)

	Ref	Expression
Assertion	elrng	$$⊢A\in V\to \left(A\in \mathrm{ran}B\leftrightarrow \exists xxBA\right)$$

Proof

Step	Hyp	Ref	Expression
1		elrn2g	$$⊢A\in V\to \left(A\in \mathrm{ran}B\leftrightarrow \exists x⟨x,A⟩\in B\right)$$
2		df-br	$$⊢xBA\leftrightarrow ⟨x,A⟩\in B$$
3	2	exbii	$$⊢\exists xxBA\leftrightarrow \exists x⟨x,A⟩\in B$$
4	1 3	bitr4di	$$⊢A\in V\to \left(A\in \mathrm{ran}B\leftrightarrow \exists xxBA\right)$$