Theorem elrn

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

	Ref	Expression
Hypothesis	elrn.1	$$⊢A\in \mathrm{V}$$
Assertion	elrn	$$⊢A\in \mathrm{ran}B\leftrightarrow \exists xxBA$$

Proof

Step	Hyp	Ref	Expression
1		elrn.1	$$⊢A\in \mathrm{V}$$
2	1	elrn2	$$⊢A\in \mathrm{ran}B\leftrightarrow \exists x⟨x,A⟩\in B$$
3		df-br	$$⊢xBA\leftrightarrow ⟨x,A⟩\in B$$
4	3	exbii	$$⊢\exists xxBA\leftrightarrow \exists x⟨x,A⟩\in B$$
5	2 4	bitr4i	$$⊢A\in \mathrm{ran}B\leftrightarrow \exists xxBA$$