Theorem fvresval

Description: The value of a restricted function at a class is either the empty set or the value of the unrestricted function at that class. (Contributed by Scott Fenton, 4-Sep-2011)

	Ref	Expression
Assertion	fvresval	$$⊢\left(\left({F\upharpoonright }_B\right)\left(A\right)=F\left(A\right)\vee \left({F\upharpoonright }_B\right)\left(A\right)=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		exmid	$$⊢\left(A\in B\vee \neg A\in B\right)$$
2		fvres	$$⊢A\in B\to \left({F\upharpoonright }_B\right)\left(A\right)=F\left(A\right)$$
3		nfvres	$$⊢\neg A\in B\to \left({F\upharpoonright }_B\right)\left(A\right)=\varnothing$$
4	2 3	orim12i	$$⊢\left(A\in B\vee \neg A\in B\right)\to \left(\left({F\upharpoonright }_B\right)\left(A\right)=F\left(A\right)\vee \left({F\upharpoonright }_B\right)\left(A\right)=\varnothing \right)$$
5	1 4	ax-mp	$$⊢\left(\left({F\upharpoonright }_B\right)\left(A\right)=F\left(A\right)\vee \left({F\upharpoonright }_B\right)\left(A\right)=\varnothing \right)$$