Theorem afv0nbfvbi

Description: The function's value at an argument is an element of a set if and only if the value of the alternative function at this argument is an element of that set, if the set does not contain the empty set. (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	afv0nbfvbi	$$⊢\varnothing \notin B\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)\in B\leftrightarrow F\left(A\right)\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		afvvfveq	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)\in B\to \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=F\left(A\right)$$
2		eleq1	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=F\left(A\right)\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)\in B\leftrightarrow F\left(A\right)\in B\right)$$
3	2	biimpd	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=F\left(A\right)\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)\in B\to F\left(A\right)\in B\right)$$
4	1 3	mpcom	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)\in B\to F\left(A\right)\in B$$
5		elnelne2	$$⊢\left(F\left(A\right)\in B\wedge \varnothing \notin B\right)\to F\left(A\right)\ne \varnothing$$
6	5	ancoms	$$⊢\left(\varnothing \notin B\wedge F\left(A\right)\in B\right)\to F\left(A\right)\ne \varnothing$$
7		fvfundmfvn0	$$⊢F\left(A\right)\ne \varnothing \to \left(A\in \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)$$
8		df-dfat	$$⊢F\mathrm{defAt}A\leftrightarrow \left(A\in \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)$$
9		afvfundmfveq	$$⊢F\mathrm{defAt}A\to \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=F\left(A\right)$$
10	8 9	sylbir	$$⊢\left(A\in \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)\to \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=F\left(A\right)$$
11		eleq1	$$⊢F\left(A\right)=\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)\to \left(F\left(A\right)\in B\leftrightarrow \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)\in B\right)$$
12	11	eqcoms	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=F\left(A\right)\to \left(F\left(A\right)\in B\leftrightarrow \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)\in B\right)$$
13	12	biimpd	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=F\left(A\right)\to \left(F\left(A\right)\in B\to \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)\in B\right)$$
14	6 7 10 13	4syl	$$⊢\left(\varnothing \notin B\wedge F\left(A\right)\in B\right)\to \left(F\left(A\right)\in B\to \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)\in B\right)$$
15	14	ex	$$⊢\varnothing \notin B\to \left(F\left(A\right)\in B\to \left(F\left(A\right)\in B\to \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)\in B\right)\right)$$
16	15	pm2.43d	$$⊢\varnothing \notin B\to \left(F\left(A\right)\in B\to \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)\in B\right)$$
17	4 16	impbid2	$$⊢\varnothing \notin B\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)\in B\leftrightarrow F\left(A\right)\in B\right)$$