MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpsneng Unicode version

Theorem xpsneng 7123
Description: A set is equinumerous to its cross-product with a singleton. Proposition 4.22(c) of [Mendelson] p. 254. (Contributed by NM, 22-Oct-2004.)
Assertion
Ref Expression
xpsneng  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  X.  { B } )  ~~  A
)

Proof of Theorem xpsneng
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xpeq1 4826 . . 3  |-  ( x  =  A  ->  (
x  X.  { y } )  =  ( A  X.  { y } ) )
2 id 20 . . 3  |-  ( x  =  A  ->  x  =  A )
31, 2breq12d 4160 . 2  |-  ( x  =  A  ->  (
( x  X.  {
y } )  ~~  x 
<->  ( A  X.  {
y } )  ~~  A ) )
4 sneq 3762 . . . 4  |-  ( y  =  B  ->  { y }  =  { B } )
54xpeq2d 4836 . . 3  |-  ( y  =  B  ->  ( A  X.  { y } )  =  ( A  X.  { B }
) )
65breq1d 4157 . 2  |-  ( y  =  B  ->  (
( A  X.  {
y } )  ~~  A 
<->  ( A  X.  { B } )  ~~  A
) )
7 vex 2896 . . 3  |-  x  e. 
_V
8 vex 2896 . . 3  |-  y  e. 
_V
97, 8xpsnen 7122 . 2  |-  ( x  X.  { y } )  ~~  x
103, 6, 9vtocl2g 2952 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  X.  { B } )  ~~  A
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1717   {csn 3751   class class class wbr 4147    X. cxp 4810    ~~ cen 7036
This theorem is referenced by:  xp1en  7124  xpsnen2g  7131  xpdom3  7136  disjen  7194  unxpdom2  7247  sucxpdom  7248  uncdadom  7978  cdaun  7979  cdaen  7980  cda1dif  7983  cdacomen  7988  cdaassen  7989  xpcdaen  7990  mapcdaen  7991  cdaxpdom  7996  cdafi  7997  cdainf  7999  infcda1  8000  pwcdadom  8023  isfin4-3  8122  pwcdandom  8469  gchxpidm  8471
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2362  ax-sep 4265  ax-nul 4273  ax-pow 4312  ax-pr 4338  ax-un 4635
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2236  df-mo 2237  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2506  df-ne 2546  df-ral 2648  df-rex 2649  df-rab 2652  df-v 2895  df-dif 3260  df-un 3262  df-in 3264  df-ss 3271  df-nul 3566  df-if 3677  df-pw 3738  df-sn 3757  df-pr 3758  df-op 3760  df-uni 3952  df-int 3987  df-br 4148  df-opab 4202  df-mpt 4203  df-id 4433  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-fun 5390  df-fn 5391  df-f 5392  df-f1 5393  df-fo 5394  df-f1o 5395  df-en 7040
  Copyright terms: Public domain W3C validator