Theorem setrec2lem1

Description: Lemma for setrec2 . The functional part of F has the same values as F . (Contributed by Emmett Weisz, 4-Mar-2021) (New usage is discouraged.)

	Ref	Expression
Assertion	setrec2lem1	$$⊢\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)\left(a\right)=F\left(a\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvres	$$⊢a\in \left\{x|\exists !yxFy\right\}\to \left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)\left(a\right)=F\left(a\right)$$
2		nfvres	$$⊢\neg a\in \left\{x|\exists !yxFy\right\}\to \left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)\left(a\right)=\varnothing$$
3		vex	$$⊢a\in \mathrm{V}$$
4		breq1	$$⊢x=a\to \left(xFy\leftrightarrow aFy\right)$$
5	4	eubidv	$$⊢x=a\to \left(\exists !yxFy\leftrightarrow \exists !yaFy\right)$$
6	3 5	elab	$$⊢a\in \left\{x|\exists !yxFy\right\}\leftrightarrow \exists !yaFy$$
7		tz6.12-2	$$⊢\neg \exists !yaFy\to F\left(a\right)=\varnothing$$
8	6 7	sylnbi	$$⊢\neg a\in \left\{x|\exists !yxFy\right\}\to F\left(a\right)=\varnothing$$
9	2 8	eqtr4d	$$⊢\neg a\in \left\{x|\exists !yxFy\right\}\to \left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)\left(a\right)=F\left(a\right)$$
10	1 9	pm2.61i	$$⊢\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)\left(a\right)=F\left(a\right)$$