# Metamath Proof Explorer

## Theorem xpsnen2g

Description: A set is equinumerous to its Cartesian product with a singleton on the left. (Contributed by Stefan O'Rear, 21-Nov-2014)

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

### Proof

Step Hyp Ref Expression
1 snex ${⊢}\left\{{A}\right\}\in \mathrm{V}$
2 xpcomeng ${⊢}\left(\left\{{A}\right\}\in \mathrm{V}\wedge {B}\in {W}\right)\to \left(\left\{{A}\right\}×{B}\right)\approx \left({B}×\left\{{A}\right\}\right)$
3 1 2 mpan ${⊢}{B}\in {W}\to \left(\left\{{A}\right\}×{B}\right)\approx \left({B}×\left\{{A}\right\}\right)$
4 xpsneng ${⊢}\left({B}\in {W}\wedge {A}\in {V}\right)\to \left({B}×\left\{{A}\right\}\right)\approx {B}$
5 4 ancoms ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left({B}×\left\{{A}\right\}\right)\approx {B}$
6 entr ${⊢}\left(\left(\left\{{A}\right\}×{B}\right)\approx \left({B}×\left\{{A}\right\}\right)\wedge \left({B}×\left\{{A}\right\}\right)\approx {B}\right)\to \left(\left\{{A}\right\}×{B}\right)\approx {B}$
7 3 5 6 syl2an2 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left\{{A}\right\}×{B}\right)\approx {B}$