Theorem bj-restsn

Description: An elementwise intersection on the singleton on a set is the singleton on the intersection by that set. Generalization of bj-restsn0 and bj-restsnid . (Contributed by BJ, 27-Apr-2021)

	Ref	Expression
Assertion	bj-restsn	$$⊢\left(Y\in V\wedge A\in W\right)\to \left\{Y\right\}{\upharpoonright }_{𝑡}A=\left\{Y\cap A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		snex	$$⊢\left\{Y\right\}\in \mathrm{V}$$
2		elrest	$$⊢\left(\left\{Y\right\}\in \mathrm{V}\wedge A\in W\right)\to \left(x\in \left(\left\{Y\right\}{\upharpoonright }_{𝑡}A\right)\leftrightarrow \exists y\in \left\{Y\right\}x=y\cap A\right)$$
3	1 2	mpan	$$⊢A\in W\to \left(x\in \left(\left\{Y\right\}{\upharpoonright }_{𝑡}A\right)\leftrightarrow \exists y\in \left\{Y\right\}x=y\cap A\right)$$
4		velsn	$$⊢x\in \left\{y\cap A\right\}\leftrightarrow x=y\cap A$$
5		ineq1	$$⊢y=Y\to y\cap A=Y\cap A$$
6	5	sneqd	$$⊢y=Y\to \left\{y\cap A\right\}=\left\{Y\cap A\right\}$$
7	6	eleq2d	$$⊢y=Y\to \left(x\in \left\{y\cap A\right\}\leftrightarrow x\in \left\{Y\cap A\right\}\right)$$
8	4 7	bitr3id	$$⊢y=Y\to \left(x=y\cap A\leftrightarrow x\in \left\{Y\cap A\right\}\right)$$
9	8	rexsng	$$⊢Y\in V\to \left(\exists y\in \left\{Y\right\}x=y\cap A\leftrightarrow x\in \left\{Y\cap A\right\}\right)$$
10	3 9	sylan9bbr	$$⊢\left(Y\in V\wedge A\in W\right)\to \left(x\in \left(\left\{Y\right\}{\upharpoonright }_{𝑡}A\right)\leftrightarrow x\in \left\{Y\cap A\right\}\right)$$
11	10	eqrdv	$$⊢\left(Y\in V\wedge A\in W\right)\to \left\{Y\right\}{\upharpoonright }_{𝑡}A=\left\{Y\cap A\right\}$$