Theorem ressn

Description: Restriction of a class to a singleton. (Contributed by Mario Carneiro, 28-Dec-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022)

	Ref	Expression
Assertion	ressn	$$⊢{A\upharpoonright }_{\left\{B\right\}}=\left\{B\right\}\times A\left[\left\{B\right\}\right]$$

Proof

Step	Hyp	Ref	Expression
1		relres	$$⊢\mathrm{Rel}\left({A\upharpoonright }_{\left\{B\right\}}\right)$$
2		relxp	$$⊢\mathrm{Rel}\left(\left\{B\right\}\times A\left[\left\{B\right\}\right]\right)$$
3		vex	$$⊢x\in \mathrm{V}$$
4		vex	$$⊢y\in \mathrm{V}$$
5	3 4	elimasn	$$⊢y\in A\left[\left\{x\right\}\right]\leftrightarrow ⟨x,y⟩\in A$$
6		elsni	$$⊢x\in \left\{B\right\}\to x=B$$
7	6	sneqd	$$⊢x\in \left\{B\right\}\to \left\{x\right\}=\left\{B\right\}$$
8	7	imaeq2d	$$⊢x\in \left\{B\right\}\to A\left[\left\{x\right\}\right]=A\left[\left\{B\right\}\right]$$
9	8	eleq2d	$$⊢x\in \left\{B\right\}\to \left(y\in A\left[\left\{x\right\}\right]\leftrightarrow y\in A\left[\left\{B\right\}\right]\right)$$
10	5 9	bitr3id	$$⊢x\in \left\{B\right\}\to \left(⟨x,y⟩\in A\leftrightarrow y\in A\left[\left\{B\right\}\right]\right)$$
11	10	pm5.32i	$$⊢\left(x\in \left\{B\right\}\wedge ⟨x,y⟩\in A\right)\leftrightarrow \left(x\in \left\{B\right\}\wedge y\in A\left[\left\{B\right\}\right]\right)$$
12	4	opelresi	$$⊢⟨x,y⟩\in \left({A\upharpoonright }_{\left\{B\right\}}\right)\leftrightarrow \left(x\in \left\{B\right\}\wedge ⟨x,y⟩\in A\right)$$
13		opelxp	$$⊢⟨x,y⟩\in \left(\left\{B\right\}\times A\left[\left\{B\right\}\right]\right)\leftrightarrow \left(x\in \left\{B\right\}\wedge y\in A\left[\left\{B\right\}\right]\right)$$
14	11 12 13	3bitr4i	$$⊢⟨x,y⟩\in \left({A\upharpoonright }_{\left\{B\right\}}\right)\leftrightarrow ⟨x,y⟩\in \left(\left\{B\right\}\times A\left[\left\{B\right\}\right]\right)$$
15	1 2 14	eqrelriiv	$$⊢{A\upharpoonright }_{\left\{B\right\}}=\left\{B\right\}\times A\left[\left\{B\right\}\right]$$