Theorem eliman0

Description: A nonempty function value is an element of the image of the function. (Contributed by Thierry Arnoux, 25-Jun-2019)

	Ref	Expression
Assertion	eliman0	$$⊢\left(A\in B\wedge \neg F\left(A\right)=\varnothing \right)\to F\left(A\right)\in F\left[B\right]$$

Proof

Step	Hyp	Ref	Expression
1		fvbr0	$$⊢\left(AFF\left(A\right)\vee F\left(A\right)=\varnothing \right)$$
2		orcom	$$⊢\left(AFF\left(A\right)\vee F\left(A\right)=\varnothing \right)\leftrightarrow \left(F\left(A\right)=\varnothing \vee AFF\left(A\right)\right)$$
3	1 2	mpbi	$$⊢\left(F\left(A\right)=\varnothing \vee AFF\left(A\right)\right)$$
4	3	ori	$$⊢\neg F\left(A\right)=\varnothing \to AFF\left(A\right)$$
5		breq1	$$⊢x=A\to \left(xFF\left(A\right)\leftrightarrow AFF\left(A\right)\right)$$
6	5	rspcev	$$⊢\left(A\in B\wedge AFF\left(A\right)\right)\to \exists x\in BxFF\left(A\right)$$
7	4 6	sylan2	$$⊢\left(A\in B\wedge \neg F\left(A\right)=\varnothing \right)\to \exists x\in BxFF\left(A\right)$$
8		fvex	$$⊢F\left(A\right)\in \mathrm{V}$$
9	8	elima	$$⊢F\left(A\right)\in F\left[B\right]\leftrightarrow \exists x\in BxFF\left(A\right)$$
10	7 9	sylibr	$$⊢\left(A\in B\wedge \neg F\left(A\right)=\varnothing \right)\to F\left(A\right)\in F\left[B\right]$$