Theorem xpsneng

Description: A set is equinumerous to its Cartesian product with a singleton. Proposition 4.22(c) of Mendelson p. 254. (Contributed by NM, 22-Oct-2004)

	Ref	Expression
Assertion	xpsneng	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\times \left\{B\right\}\right)\approx A$$

Proof

Step	Hyp	Ref	Expression
1		xpeq1	$$⊢x=A\to x\times \left\{y\right\}=A\times \left\{y\right\}$$
2		id	$$⊢x=A\to x=A$$
3	1 2	breq12d	$$⊢x=A\to \left(\left(x\times \left\{y\right\}\right)\approx x\leftrightarrow \left(A\times \left\{y\right\}\right)\approx A\right)$$
4		sneq	$$⊢y=B\to \left\{y\right\}=\left\{B\right\}$$
5	4	xpeq2d	$$⊢y=B\to A\times \left\{y\right\}=A\times \left\{B\right\}$$
6	5	breq1d	$$⊢y=B\to \left(\left(A\times \left\{y\right\}\right)\approx A\leftrightarrow \left(A\times \left\{B\right\}\right)\approx A\right)$$
7		vex	$$⊢x\in \mathrm{V}$$
8		vex	$$⊢y\in \mathrm{V}$$
9	7 8	xpsnen	$$⊢\left(x\times \left\{y\right\}\right)\approx x$$
10	3 6 9	vtocl2g	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\times \left\{B\right\}\right)\approx A$$