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

Theorem xpss12 5563
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 3958 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
2 ssel 3958 . . . 4 (𝐶𝐷 → (𝑦𝐶𝑦𝐷))
31, 2im2anan9 619 . . 3 ((𝐴𝐵𝐶𝐷) → ((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐷)))
43ssopab2dv 5429 . 2 ((𝐴𝐵𝐶𝐷) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐷)})
5 df-xp 5554 . 2 (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)}
6 df-xp 5554 . 2 (𝐵 × 𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐷)}
74, 5, 63sstr4g 4009 1 ((𝐴𝐵𝐶𝐷) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105  wss 3933  {copab 5119   × cxp 5546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-in 3940  df-ss 3949  df-opab 5120  df-xp 5554
This theorem is referenced by:  xpss  5564  inxpssres  5565  xpss1  5567  xpss2  5568  djussxp  5709  ssxpb  6024  cossxp  6116  relrelss  6117  fssxp  6527  oprabss  7249  oprres  7305  fimaproj  7818  pmss12g  8422  marypha1lem  8885  marypha2lem1  8887  hartogslem1  8994  infxpenlem  9427  dfac5lem4  9540  axdc4lem  9865  fpwwe2lem1  10041  fpwwe2lem11  10050  fpwwe2lem12  10051  fpwwe2lem13  10052  canthwe  10061  tskxpss  10182  dmaddpi  10300  dmmulpi  10301  addnqf  10358  mulnqf  10359  rexpssxrxp  10674  ltrelxr  10690  mulnzcnopr  11274  dfz2  11988  elq  12338  leiso  13805  znnen  15553  phimullem  16104  imasless  16801  sscpwex  17073  fullsubc  17108  fullresc  17109  wunfunc  17157  funcres2c  17159  homaf  17278  dmcoass  17314  catcoppccl  17356  catcfuccl  17357  catcxpccl  17445  znleval  20629  txuni2  22101  txbas  22103  txcld  22139  txcls  22140  neitx  22143  txcnp  22156  txlly  22172  txnlly  22173  hausdiag  22181  tx1stc  22186  txkgen  22188  xkococnlem  22195  cnmpt2res  22213  clssubg  22644  tsmsxplem1  22688  tsmsxplem2  22689  tsmsxp  22690  trust  22765  ustuqtop1  22777  psmetres2  22851  xmetres2  22898  metres2  22900  ressprdsds  22908  xmetresbl  22974  ressxms  23062  metustexhalf  23093  cfilucfil  23096  restmetu  23107  nrginvrcn  23228  qtopbaslem  23294  tgqioo  23335  re2ndc  23336  resubmet  23337  xrsdsre  23345  bndth  23489  lebnumii  23497  iscfil2  23796  cmssmscld  23880  cmsss  23881  cmscsscms  23903  minveclem3a  23957  ovolfsf  23999  opnmblALT  24131  mbfimaopnlem  24183  itg1addlem4  24227  limccnp2  24417  taylfval  24874  taylf  24876  dvdsmulf1o  25698  fsumdvdsmul  25699  sspg  28432  ssps  28434  sspmlem  28436  issh2  28913  hhssabloilem  28965  hhssabloi  28966  hhssnv  28968  hhshsslem1  28971  shsel  29018  ofrn2  30315  gtiso  30362  xrofsup  30418  txomap  30997  tpr2rico  31054  prsss  31058  raddcn  31071  xrge0pluscn  31082  br2base  31426  dya2iocnrect  31438  dya2iocucvr  31441  eulerpartlemgh  31535  eulerpartlemgs2  31537  cvmlift2lem9  32455  cvmlift2lem10  32456  cvmlift2lem11  32457  cvmlift2lem12  32458  mpstssv  32683  elxp8  34534  mblfinlem2  34811  ftc1anc  34856  ssbnd  34947  prdsbnd2  34954  cnpwstotbnd  34956  reheibor  34998  exidreslem  35036  divrngcl  35116  isdrngo2  35117  dibss  38185  xppss12  38993  arearect  39700  rtrclex  39855  rtrclexi  39859  rp-imass  39995  rr2sscn2  41510  fourierdlem42  42311  opnvonmbllem2  42792  rnghmresfn  44162  rnghmsscmap2  44172  rnghmsscmap  44173  rhmresfn  44208  rhmsscmap2  44218  rhmsscmap  44219  rhmsscrnghm  44225  rngcrescrhm  44284  rngcrescrhmALTV  44302
  Copyright terms: Public domain W3C validator