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	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 × 1o ) ≈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df1o2	⊢ 1o = { ∅ }
2	1	xpeq2i	⊢ ( 𝐴 × 1o ) = ( 𝐴 × { ∅ } )
3		0ex	⊢ ∅ ∈ V
4		xpsneng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∅ ∈ V ) → ( 𝐴 × { ∅ } ) ≈ 𝐴 )
5	3 4	mpan2	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 × { ∅ } ) ≈ 𝐴 )
6	2 5	eqbrtrid	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 × 1o ) ≈ 𝐴 )