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 | |- ( ( A e. V /\ B e. W ) -> ( A X. { B } ) ~~ A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xpeq1 | |- ( x = A -> ( x X. { y } ) = ( A X. { y } ) ) |
|
| 2 | id | |- ( x = A -> x = A ) |
|
| 3 | 1 2 | breq12d | |- ( x = A -> ( ( x X. { y } ) ~~ x <-> ( A X. { y } ) ~~ A ) ) |
| 4 | sneq | |- ( y = B -> { y } = { B } ) |
|
| 5 | 4 | xpeq2d | |- ( y = B -> ( A X. { y } ) = ( A X. { B } ) ) |
| 6 | 5 | breq1d | |- ( y = B -> ( ( A X. { y } ) ~~ A <-> ( A X. { B } ) ~~ A ) ) |
| 7 | vex | |- x e. _V |
|
| 8 | vex | |- y e. _V |
|
| 9 | 7 8 | xpsnen | |- ( x X. { y } ) ~~ x |
| 10 | 3 6 9 | vtocl2g | |- ( ( A e. V /\ B e. W ) -> ( A X. { B } ) ~~ A ) |