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

Theorem xpss12 5215
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 3589 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
2 ssel 3589 . . . 4 (𝐶𝐷 → (𝑦𝐶𝑦𝐷))
31, 2im2anan9 879 . . 3 ((𝐴𝐵𝐶𝐷) → ((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐷)))
43ssopab2dv 4994 . 2 ((𝐴𝐵𝐶𝐷) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐷)})
5 df-xp 5110 . 2 (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)}
6 df-xp 5110 . 2 (𝐵 × 𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐷)}
74, 5, 63sstr4g 3638 1 ((𝐴𝐵𝐶𝐷) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 1988  wss 3567  {copab 4703   × cxp 5102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-in 3574  df-ss 3581  df-opab 4704  df-xp 5110
This theorem is referenced by:  xpss  5216  xpss1  5218  xpss2  5219  djussxp  5256  ssxpb  5556  ssrnres  5560  cossxp  5646  relrelss  5647  fssxp  6047  oprabss  6731  oprres  6787  pmss12g  7869  marypha1lem  8324  marypha2lem1  8326  hartogslem1  8432  infxpenlem  8821  dfac5lem4  8934  axdc4lem  9262  fpwwe2lem1  9438  fpwwe2lem11  9447  fpwwe2lem12  9448  fpwwe2lem13  9449  canthwe  9458  tskxpss  9579  dmaddpi  9697  dmmulpi  9698  addnqf  9755  mulnqf  9756  rexpssxrxp  10069  ltrelxr  10084  mulnzcnopr  10658  dfz2  11380  elq  11775  leiso  13226  znnen  14922  eucalg  15281  phimullem  15465  imasless  16181  sscpwex  16456  fullsubc  16491  fullresc  16492  wunfunc  16540  funcres2c  16542  homaf  16661  dmcoass  16697  catcoppccl  16739  catcfuccl  16740  catcxpccl  16828  znleval  19884  txuni2  21349  txbas  21351  txcld  21387  txcls  21388  neitx  21391  txcnp  21404  txlly  21420  txnlly  21421  hausdiag  21429  tx1stc  21434  txkgen  21436  xkococnlem  21443  cnmpt2res  21461  clssubg  21893  tsmsxplem1  21937  tsmsxplem2  21938  tsmsxp  21939  trust  22014  ustuqtop1  22026  psmetres2  22100  xmetres2  22147  metres2  22149  ressprdsds  22157  xmetresbl  22223  ressxms  22311  metustexhalf  22342  cfilucfil  22345  restmetu  22356  nrginvrcn  22477  qtopbaslem  22543  tgqioo  22584  re2ndc  22585  resubmet  22586  xrsdsre  22594  bndth  22738  lebnumii  22746  iscfil2  23045  cmsss  23128  minveclem3a  23179  ovolfsf  23221  opnmblALT  23352  mbfimaopnlem  23403  itg1addlem4  23447  limccnp2  23637  taylfval  24094  taylf  24096  dvdsmulf1o  24901  fsumdvdsmul  24902  sspg  27553  ssps  27555  sspmlem  27557  issh2  28036  hhssabloilem  28088  hhssabloi  28089  hhssnv  28091  hhshsslem1  28094  shsel  28143  ofrn2  29415  gtiso  29452  xrofsup  29507  fimaproj  29874  txomap  29875  tpr2rico  29932  prsss  29936  raddcn  29949  xrge0pluscn  29960  br2base  30305  dya2iocnrect  30317  dya2iocucvr  30320  eulerpartlemgh  30414  eulerpartlemgs2  30416  cvmlift2lem9  31267  cvmlift2lem10  31268  cvmlift2lem11  31269  cvmlift2lem12  31270  mpstssv  31410  elxp8  33190  mblfinlem2  33418  ftc1anc  33464  ssbnd  33558  prdsbnd2  33565  cnpwstotbnd  33567  reheibor  33609  exidreslem  33647  divrngcl  33727  isdrngo2  33728  dibss  36277  arearect  37620  rtrclex  37743  rtrclexi  37747  rp-imass  37885  idhe  37901  rr2sscn2  39395  fourierdlem42  40129  opnvonmbllem2  40610  rnghmresfn  41728  rnghmsscmap2  41738  rnghmsscmap  41739  rhmresfn  41774  rhmsscmap2  41784  rhmsscmap  41785  rhmsscrnghm  41791  rngcrescrhm  41850  rngcrescrhmALTV  41868
  Copyright terms: Public domain W3C validator