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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 × { 𝐵 } ) ≈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		xpeq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 × { 𝑦 } ) = ( 𝐴 × { 𝑦 } ) )
2		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
3	1 2	breq12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 × { 𝑦 } ) ≈ 𝑥 ↔ ( 𝐴 × { 𝑦 } ) ≈ 𝐴 ) )
4		sneq	⊢ ( 𝑦 = 𝐵 → { 𝑦 } = { 𝐵 } )
5	4	xpeq2d	⊢ ( 𝑦 = 𝐵 → ( 𝐴 × { 𝑦 } ) = ( 𝐴 × { 𝐵 } ) )
6	5	breq1d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 × { 𝑦 } ) ≈ 𝐴 ↔ ( 𝐴 × { 𝐵 } ) ≈ 𝐴 ) )
7		vex	⊢ 𝑥 ∈ V
8		vex	⊢ 𝑦 ∈ V
9	7 8	xpsnen	⊢ ( 𝑥 × { 𝑦 } ) ≈ 𝑥
10	3 6 9	vtocl2g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 × { 𝐵 } ) ≈ 𝐴 )