Theorem elunirn2OLD

Description: Obsolete version of elfvunirn as of 12-Jan-2025. (Contributed by Thierry Arnoux, 13-Nov-2016) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	elunirn2OLD	$$⊢\left(\mathrm{Fun}F\wedge B\in F\left(A\right)\right)\to B\in \bigcup \mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		elfvdm	$$⊢B\in F\left(A\right)\to A\in \mathrm{dom}F$$
2		fveq2	$$⊢x=A\to F\left(x\right)=F\left(A\right)$$
3	2	eleq2d	$$⊢x=A\to \left(B\in F\left(x\right)\leftrightarrow B\in F\left(A\right)\right)$$
4	3	rspcev	$$⊢\left(A\in \mathrm{dom}F\wedge B\in F\left(A\right)\right)\to \exists x\in \mathrm{dom}FB\in F\left(x\right)$$
5	1 4	mpancom	$$⊢B\in F\left(A\right)\to \exists x\in \mathrm{dom}FB\in F\left(x\right)$$
6	5	adantl	$$⊢\left(\mathrm{Fun}F\wedge B\in F\left(A\right)\right)\to \exists x\in \mathrm{dom}FB\in F\left(x\right)$$
7		elunirn	$$⊢\mathrm{Fun}F\to \left(B\in \bigcup \mathrm{ran}F\leftrightarrow \exists x\in \mathrm{dom}FB\in F\left(x\right)\right)$$
8	7	adantr	$$⊢\left(\mathrm{Fun}F\wedge B\in F\left(A\right)\right)\to \left(B\in \bigcup \mathrm{ran}F\leftrightarrow \exists x\in \mathrm{dom}FB\in F\left(x\right)\right)$$
9	6 8	mpbird	$$⊢\left(\mathrm{Fun}F\wedge B\in F\left(A\right)\right)\to B\in \bigcup \mathrm{ran}F$$