Theorem xp1en

Description: One times a cardinal number. (Contributed by NM, 27-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

	Ref	Expression
Assertion	xp1en	$$⊢A\in V\to \left(A\times 1_{𝑜}\right)\approx A$$

Proof

Step	Hyp	Ref	Expression
1		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
2	1	xpeq2i	$$⊢A\times 1_{𝑜}=A\times \left\{\varnothing \right\}$$
3		0ex	$$⊢\varnothing \in \mathrm{V}$$
4		xpsneng	$$⊢\left(A\in V\wedge \varnothing \in \mathrm{V}\right)\to \left(A\times \left\{\varnothing \right\}\right)\approx A$$
5	3 4	mpan2	$$⊢A\in V\to \left(A\times \left\{\varnothing \right\}\right)\approx A$$
6	2 5	eqbrtrid	$$⊢A\in V\to \left(A\times 1_{𝑜}\right)\approx A$$