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

Theorem xpss12 5700
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 3977 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
2 ssel 3977 . . . 4 (𝐶𝐷 → (𝑦𝐶𝑦𝐷))
31, 2im2anan9 620 . . 3 ((𝐴𝐵𝐶𝐷) → ((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐷)))
43ssopab2dv 5556 . 2 ((𝐴𝐵𝐶𝐷) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐷)})
5 df-xp 5691 . 2 (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)}
6 df-xp 5691 . 2 (𝐵 × 𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐷)}
74, 5, 63sstr4g 4037 1 ((𝐴𝐵𝐶𝐷) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2108  wss 3951  {copab 5205   × cxp 5683
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-opab 5206  df-xp 5691
This theorem is referenced by:  xpss  5701  inxpssres  5702  xpss1  5704  xpss2  5705  djussxp  5856  ssxpb  6194  resssxp  6290  cossxp  6292  relrelss  6293  fssxp  6763  oprabss  7541  oprres  7601  fimaproj  8160  xpord2pred  8170  xpord3pred  8177  naddcllem  8714  naddov2  8717  naddunif  8731  naddasslem1  8732  naddasslem2  8733  pmss12g  8909  marypha1lem  9473  marypha2lem1  9475  hartogslem1  9582  infxpenlem  10053  dfac5lem4  10166  dfac5lem4OLD  10168  axdc4lem  10495  fpwwe2lem1  10671  fpwwe2lem10  10680  fpwwe2lem11  10681  fpwwe2lem12  10682  canthwe  10691  tskxpss  10812  dmaddpi  10930  dmmulpi  10931  addnqf  10988  mulnqf  10989  rexpssxrxp  11306  ltrelxr  11322  mulnzcnf  11909  dfz2  12632  elq  12992  leiso  14498  znnen  16248  phimullem  16816  imasless  17585  sscpwex  17859  fullsubc  17895  fullresc  17896  wunfunc  17946  funcres2c  17948  homaf  18075  dmcoass  18111  catcoppccl  18162  catcfuccl  18163  catcxpccl  18252  rnghmresfn  20619  rnghmsscmap2  20629  rnghmsscmap  20630  rhmresfn  20648  rhmsscmap2  20658  rhmsscmap  20659  rhmsscrnghm  20665  rngcrescrhm  20684  znleval  21573  txuni2  23573  txbas  23575  txcld  23611  txcls  23612  neitx  23615  txcnp  23628  txlly  23644  txnlly  23645  hausdiag  23653  tx1stc  23658  txkgen  23660  xkococnlem  23667  cnmpt2res  23685  clssubg  24117  tsmsxplem1  24161  tsmsxplem2  24162  tsmsxp  24163  trust  24238  ustuqtop1  24250  psmetres2  24324  xmetres2  24371  metres2  24373  ressprdsds  24381  xmetresbl  24447  ressxms  24538  metustexhalf  24569  cfilucfil  24572  restmetu  24583  nrginvrcn  24713  qtopbaslem  24779  tgqioo  24821  re2ndc  24822  resubmet  24823  xrsdsre  24832  bndth  24990  lebnumii  24998  iscfil2  25300  cmssmscld  25384  cmsss  25385  cmscsscms  25407  minveclem3a  25461  ovolfsf  25506  opnmblALT  25638  mbfimaopnlem  25690  itg1addlem4  25734  limccnp2  25927  taylfval  26400  taylf  26402  mpodvdsmulf1o  27237  fsumdvdsmul  27238  dvdsmulf1o  27239  fsumdvdsmulOLD  27240  elzs  28370  sspg  30747  ssps  30749  sspmlem  30751  issh2  31228  hhssabloilem  31280  hhssabloi  31281  hhssnv  31283  hhshsslem1  31286  shsel  31333  iunxpssiun1  32581  ofrn2  32650  djussxp2  32658  gtiso  32710  xrofsup  32771  gsumwrd2dccatlem  33069  txomap  33833  tpr2rico  33911  prsss  33915  raddcn  33928  xrge0pluscn  33939  br2base  34271  dya2iocnrect  34283  dya2iocucvr  34286  eulerpartlemgh  34380  eulerpartlemgs2  34382  cvmlift2lem9  35316  cvmlift2lem10  35317  cvmlift2lem11  35318  cvmlift2lem12  35319  mpstssv  35544  elxp8  37372  mblfinlem2  37665  ftc1anc  37708  ssbnd  37795  prdsbnd2  37802  cnpwstotbnd  37804  reheibor  37846  exidreslem  37884  divrngcl  37964  isdrngo2  37965  dibss  41171  xppss12  42268  arearect  43227  rtrclex  43630  rtrclexi  43634  rr2sscn2  45377  fourierdlem42  46164  opnvonmbllem2  46648  rngcrescrhmALTV  48196
  Copyright terms: Public domain W3C validator