Theorem afv0fv0

Description: If the value of the alternative function at an argument is the empty set, the function's value at this argument is the empty set. (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	afv0fv0	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\varnothing \to F\left(A\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2		eleq1a	$$⊢\varnothing \in \mathrm{V}\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\varnothing \to \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)\in \mathrm{V}\right)$$
3	1 2	ax-mp	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\varnothing \to \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)\in \mathrm{V}$$
4		afvvfveq	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)\in \mathrm{V}\to \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=F\left(A\right)$$
5		eqeq1	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=F\left(A\right)\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\varnothing \leftrightarrow F\left(A\right)=\varnothing \right)$$
6	5	biimpd	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=F\left(A\right)\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\varnothing \to F\left(A\right)=\varnothing \right)$$
7	4 6	syl	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)\in \mathrm{V}\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\varnothing \to F\left(A\right)=\varnothing \right)$$
8	3 7	mpcom	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\varnothing \to F\left(A\right)=\varnothing$$