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

Theorem xpss12 5096
Description: Subset theorem for Cartesian product. Generalization of Theorem 101 of [Suppes] p. 52. (Contributed by NM, 26-Aug-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
xpss12  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( A  X.  C
)  C_  ( B  X.  D ) )

Proof of Theorem xpss12
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssel 3483 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
2 ssel 3483 . . . 4  |-  ( C 
C_  D  ->  (
y  e.  C  -> 
y  e.  D ) )
31, 2im2anan9 833 . . 3  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( ( x  e.  A  /\  y  e.  C )  ->  (
x  e.  B  /\  y  e.  D )
) )
43ssopab2dv 4765 . 2  |-  ( ( A  C_  B  /\  C  C_  D )  ->  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }  C_  {
<. x ,  y >.  |  ( x  e.  B  /\  y  e.  D ) } )
5 df-xp 4994 . 2  |-  ( A  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }
6 df-xp 4994 . 2  |-  ( B  X.  D )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  D ) }
74, 5, 63sstr4g 3530 1  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( A  X.  C
)  C_  ( B  X.  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1823    C_ wss 3461   {copab 4496    X. cxp 4986
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-in 3468  df-ss 3475  df-opab 4498  df-xp 4994
This theorem is referenced by:  xpss  5097  xpss1  5099  xpss2  5100  djussxp  5137  ssxpb  5426  ssrnres  5430  cossxp  5513  relrelss  5514  fssxp  5725  oprabss  6361  pmss12g  7438  marypha1lem  7885  marypha2lem1  7887  hartogslem1  7959  infxpenlem  8382  dfac5lem4  8498  axdc4lem  8826  fpwwe2lem1  8998  fpwwe2lem11  9007  fpwwe2lem12  9008  fpwwe2lem13  9009  canthwe  9018  tskxpss  9139  dmaddpi  9257  dmmulpi  9258  addnqf  9315  mulnqf  9316  rexpssxrxp  9627  ltrelxr  9637  mulnzcnopr  10191  dfz2  10878  elq  11185  leiso  12495  xpnnenOLD  14030  znnen  14033  eucalg  14303  phimullem  14396  imasless  15032  sscpwex  15306  fullsubc  15341  fullresc  15342  wunfunc  15390  funcres2c  15392  homaf  15511  dmcoass  15547  catcoppccl  15589  catcfuccl  15590  catcxpccl  15678  znleval  18769  txuni2  20235  txbas  20237  txcld  20273  txcls  20274  neitx  20277  txcnp  20290  txlly  20306  txnlly  20307  hausdiag  20315  tx1stc  20320  txkgen  20322  xkococnlem  20329  cnmpt2res  20347  clssubg  20776  tsmsxplem1  20824  tsmsxplem2  20825  tsmsxp  20826  trust  20901  ustuqtop1  20913  psmetres2  20987  xmetres2  21033  metres2  21035  ressprdsds  21043  xmetresbl  21109  ressxms  21197  metustexhalfOLD  21235  metustexhalf  21236  cfilucfilOLD  21241  cfilucfil  21242  restmetu  21259  nrginvrcn  21369  qtopbaslem  21434  tgqioo  21474  re2ndc  21475  resubmet  21476  xrsdsre  21484  bndth  21627  lebnumii  21635  iscfil2  21874  cmsss  21958  minveclem3a  22011  ovolfsf  22052  opnmblALT  22181  mbfimaopnlem  22231  itg1addlem4  22275  limccnp2  22465  taylfval  22923  taylf  22925  dvdsmulf1o  23671  fsumdvdsmul  23672  resgrprn  25483  issubgoi  25513  ghgrpOLD  25571  sspg  25842  ssps  25844  sspmlem  25846  issh2  26327  hhssabloi  26379  hhssnv  26381  hhshsslem1  26384  shsel  26433  ofrn2  27704  gtiso  27750  xrofsup  27819  fimaproj  28074  txomap  28075  tpr2rico  28132  prsss  28136  raddcn  28149  xrge0pluscn  28160  br2base  28480  dya2iocnrect  28492  dya2iocucvr  28495  eulerpartlemgh  28584  eulerpartlemgs2  28586  cvmlift2lem9  29023  cvmlift2lem10  29024  cvmlift2lem11  29025  cvmlift2lem12  29026  mpstssv  29166  ghomfo  29298  mblfinlem2  30295  ftc1anc  30341  ssbnd  30527  prdsbnd2  30534  cnpwstotbnd  30536  reheibor  30578  exidreslem  30582  divrngcl  30603  isdrngo2  30604  arearect  31427  fourierdlem42  32173  rnghmresfn  33044  rnghmsscmap2  33054  rnghmsscmap  33055  rhmresfn  33090  rhmsscmap2  33100  rhmsscmap  33101  rhmsscrnghm  33107  rngcrescrhm  33166  rngcrescrhmALTV  33185  dibss  37312  rp-imass  38268  idhe  38284
  Copyright terms: Public domain W3C validator