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

Theorem xpss12 5113
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

Proof of Theorem xpss12
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssel 3497 . . . 4
2 ssel 3497 . . . 4
31, 2im2anan9 835 . . 3
43ssopab2dv 4781 . 2
5 df-xp 5010 . 2
6 df-xp 5010 . 2
74, 5, 63sstr4g 3544 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  C_wss 3475  {copab 4509  X.cxp 5002
This theorem is referenced by:  xpss  5114  xpss1  5116  xpss2  5117  djussxp  5153  ssxpb  5446  ssrnres  5450  cossxp  5535  relrelss  5536  fssxp  5748  oprabss  6388  pmss12g  7465  marypha1lem  7913  marypha2lem1  7915  hartogslem1  7988  infxpenlem  8412  dfac5lem4  8528  axdc4lem  8856  fpwwe2lem1  9030  fpwwe2lem11  9039  fpwwe2lem12  9040  fpwwe2lem13  9041  canthwe  9050  tskxpss  9171  dmaddpi  9289  dmmulpi  9290  addnqf  9347  mulnqf  9348  rexpssxrxp  9659  ltrelxr  9669  mulnzcnopr  10220  dfz2  10907  elq  11213  leiso  12508  xpnnenOLD  13943  znnen  13946  eucalg  14216  phimullem  14309  imasless  14937  sscpwex  15184  fullsubc  15219  fullresc  15220  wunfunc  15268  funcres2c  15270  homaf  15357  dmcoass  15393  catcoppccl  15435  catcfuccl  15436  catcxpccl  15476  znleval  18593  txuni2  20066  txbas  20068  txcld  20104  txcls  20105  neitx  20108  txcnp  20121  txlly  20137  txnlly  20138  hausdiag  20146  tx1stc  20151  txkgen  20153  xkococnlem  20160  cnmpt2res  20178  clssubg  20607  tsmsxplem1  20655  tsmsxplem2  20656  tsmsxp  20657  trust  20732  ustuqtop1  20744  psmetres2  20818  xmetres2  20864  metres2  20866  ressprdsds  20874  xmetresbl  20940  ressxms  21028  metustexhalfOLD  21066  metustexhalf  21067  cfilucfilOLD  21072  cfilucfil  21073  restmetu  21090  nrginvrcn  21200  qtopbaslem  21265  tgqioo  21305  re2ndc  21306  resubmet  21307  xrsdsre  21315  bndth  21458  lebnumii  21466  iscfil2  21705  cmsss  21789  minveclem3a  21842  ovolfsf  21883  opnmblALT  22012  mbfimaopnlem  22062  itg1addlem4  22106  limccnp2  22296  taylfval  22754  taylf  22756  dvdsmulf1o  23470  fsumdvdsmul  23471  resgrprn  25282  issubgoi  25312  ghgrpOLD  25370  sspg  25641  ssps  25643  sspmlem  25645  issh2  26126  hhssabloi  26178  hhssnv  26180  hhshsslem1  26183  shsel  26232  ofrn2  27480  gtiso  27519  xrofsup  27582  fimaproj  27836  txomap  27837  tpr2rico  27894  prsss  27898  raddcn  27911  xrge0pluscn  27922  br2base  28240  dya2iocnrect  28252  dya2iocucvr  28255  eulerpartlemgh  28317  eulerpartlemgs2  28319  cvmlift2lem9  28756  cvmlift2lem10  28757  cvmlift2lem11  28758  cvmlift2lem12  28759  mpstssv  28899  ghomfo  29031  mblfinlem2  30052  ftc1anc  30098  ssbnd  30284  prdsbnd2  30291  cnpwstotbnd  30293  reheibor  30335  exidreslem  30339  divrngcl  30360  isdrngo2  30361  arearect  31183  fourierdlem42  31931  rnghmresfn  32771  rnghmsscmap2  32781  rnghmsscmap  32782  rhmresfn  32817  rhmsscmap2  32827  rhmsscmap  32828  rhmsscrnghm  32834  rngcrescrhm  32893  rngcrescrhmOLD  32912  dibss  36896  rp-imass  37795  idhe  37810
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-in 3482  df-ss 3489  df-opab 4511  df-xp 5010
  Copyright terms: Public domain W3C validator