Metamath Proof Explorer


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