Theorem elrn3

Description: Quantifier-free definition of membership in a range. (Contributed by Scott Fenton, 21-Jan-2017)

	Ref	Expression
Assertion	elrn3	$$⊢A\in \mathrm{ran}B\leftrightarrow B\cap \left(\mathrm{V}\times \left\{A\right\}\right)\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-rn	$$⊢\mathrm{ran}B=\mathrm{dom}{B}^{-1}$$
2	1	eleq2i	$$⊢A\in \mathrm{ran}B\leftrightarrow A\in \mathrm{dom}{B}^{-1}$$
3		eldm3	$$⊢A\in \mathrm{dom}{B}^{-1}\leftrightarrow {B^{-1}\upharpoonright }_{\left\{A\right\}}\ne \varnothing$$
4		cnvxp	$$⊢{\left(\mathrm{V}\times \left\{A\right\}\right)}^{-1}=\left\{A\right\}\times \mathrm{V}$$
5	4	ineq2i	$$⊢B^{-1}\cap {\left(\mathrm{V}\times \left\{A\right\}\right)}^{-1}=B^{-1}\cap \left(\left\{A\right\}\times \mathrm{V}\right)$$
6		cnvin	$$⊢{\left(B\cap \left(\mathrm{V}\times \left\{A\right\}\right)\right)}^{-1}=B^{-1}\cap {\left(\mathrm{V}\times \left\{A\right\}\right)}^{-1}$$
7		df-res	$$⊢{B^{-1}\upharpoonright }_{\left\{A\right\}}=B^{-1}\cap \left(\left\{A\right\}\times \mathrm{V}\right)$$
8	5 6 7	3eqtr4ri	$$⊢{B^{-1}\upharpoonright }_{\left\{A\right\}}={\left(B\cap \left(\mathrm{V}\times \left\{A\right\}\right)\right)}^{-1}$$
9	8	eqeq1i	$$⊢{B^{-1}\upharpoonright }_{\left\{A\right\}}=\varnothing \leftrightarrow {\left(B\cap \left(\mathrm{V}\times \left\{A\right\}\right)\right)}^{-1}=\varnothing$$
10		relinxp	$$⊢\mathrm{Rel}\left(B\cap \left(\mathrm{V}\times \left\{A\right\}\right)\right)$$
11		cnveq0	$$⊢\mathrm{Rel}\left(B\cap \left(\mathrm{V}\times \left\{A\right\}\right)\right)\to \left(B\cap \left(\mathrm{V}\times \left\{A\right\}\right)=\varnothing \leftrightarrow {\left(B\cap \left(\mathrm{V}\times \left\{A\right\}\right)\right)}^{-1}=\varnothing \right)$$
12	10 11	ax-mp	$$⊢B\cap \left(\mathrm{V}\times \left\{A\right\}\right)=\varnothing \leftrightarrow {\left(B\cap \left(\mathrm{V}\times \left\{A\right\}\right)\right)}^{-1}=\varnothing$$
13	9 12	bitr4i	$$⊢{B^{-1}\upharpoonright }_{\left\{A\right\}}=\varnothing \leftrightarrow B\cap \left(\mathrm{V}\times \left\{A\right\}\right)=\varnothing$$
14	13	necon3bii	$$⊢{B^{-1}\upharpoonright }_{\left\{A\right\}}\ne \varnothing \leftrightarrow B\cap \left(\mathrm{V}\times \left\{A\right\}\right)\ne \varnothing$$
15	2 3 14	3bitri	$$⊢A\in \mathrm{ran}B\leftrightarrow B\cap \left(\mathrm{V}\times \left\{A\right\}\right)\ne \varnothing$$