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

Theorem xpss12 5269
 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 3726 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
2 ssel 3726 . . . 4 (𝐶𝐷 → (𝑦𝐶𝑦𝐷))
31, 2im2anan9 916 . . 3 ((𝐴𝐵𝐶𝐷) → ((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐷)))
43ssopab2dv 5142 . 2 ((𝐴𝐵𝐶𝐷) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐷)})
5 df-xp 5260 . 2 (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)}
6 df-xp 5260 . 2 (𝐵 × 𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐷)}
74, 5, 63sstr4g 3775 1 ((𝐴𝐵𝐶𝐷) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2127   ⊆ wss 3703  {copab 4852   × cxp 5252 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-in 3710  df-ss 3717  df-opab 4853  df-xp 5260 This theorem is referenced by:  xpss  5270  xpss1  5272  xpss2  5273  djussxp  5411  ssxpb  5714  ssrnres  5718  cossxp  5807  relrelss  5808  fssxp  6209  oprabss  6899  oprres  6955  pmss12g  8038  marypha1lem  8492  marypha2lem1  8494  hartogslem1  8600  infxpenlem  8997  dfac5lem4  9110  axdc4lem  9440  fpwwe2lem1  9616  fpwwe2lem11  9625  fpwwe2lem12  9626  fpwwe2lem13  9627  canthwe  9636  tskxpss  9757  dmaddpi  9875  dmmulpi  9876  addnqf  9933  mulnqf  9934  rexpssxrxp  10247  ltrelxr  10262  mulnzcnopr  10836  dfz2  11558  elq  11954  leiso  13406  znnen  15111  eucalg  15473  phimullem  15657  imasless  16373  sscpwex  16647  fullsubc  16682  fullresc  16683  wunfunc  16731  funcres2c  16733  homaf  16852  dmcoass  16888  catcoppccl  16930  catcfuccl  16931  catcxpccl  17019  znleval  20076  txuni2  21541  txbas  21543  txcld  21579  txcls  21580  neitx  21583  txcnp  21596  txlly  21612  txnlly  21613  hausdiag  21621  tx1stc  21626  txkgen  21628  xkococnlem  21635  cnmpt2res  21653  clssubg  22084  tsmsxplem1  22128  tsmsxplem2  22129  tsmsxp  22130  trust  22205  ustuqtop1  22217  psmetres2  22291  xmetres2  22338  metres2  22340  ressprdsds  22348  xmetresbl  22414  ressxms  22502  metustexhalf  22533  cfilucfil  22536  restmetu  22547  nrginvrcn  22668  qtopbaslem  22734  tgqioo  22775  re2ndc  22776  resubmet  22777  xrsdsre  22785  bndth  22929  lebnumii  22937  iscfil2  23235  cmsss  23318  minveclem3a  23369  ovolfsf  23411  opnmblALT  23542  mbfimaopnlem  23592  itg1addlem4  23636  limccnp2  23826  taylfval  24283  taylf  24285  dvdsmulf1o  25090  fsumdvdsmul  25091  sspg  27863  ssps  27865  sspmlem  27867  issh2  28346  hhssabloilem  28398  hhssabloi  28399  hhssnv  28401  hhshsslem1  28404  shsel  28453  ofrn2  29722  gtiso  29758  xrofsup  29813  fimaproj  30180  txomap  30181  tpr2rico  30238  prsss  30242  raddcn  30255  xrge0pluscn  30266  br2base  30611  dya2iocnrect  30623  dya2iocucvr  30626  eulerpartlemgh  30720  eulerpartlemgs2  30722  cvmlift2lem9  31571  cvmlift2lem10  31572  cvmlift2lem11  31573  cvmlift2lem12  31574  mpstssv  31714  elxp8  33501  mblfinlem2  33729  ftc1anc  33775  ssbnd  33869  prdsbnd2  33876  cnpwstotbnd  33878  reheibor  33920  exidreslem  33958  divrngcl  34038  isdrngo2  34039  inxpssres  34369  dibss  36929  arearect  38272  rtrclex  38395  rtrclexi  38399  rp-imass  38536  idhe  38552  rr2sscn2  40049  fourierdlem42  40838  opnvonmbllem2  41322  rnghmresfn  42442  rnghmsscmap2  42452  rnghmsscmap  42453  rhmresfn  42488  rhmsscmap2  42498  rhmsscmap  42499  rhmsscrnghm  42505  rngcrescrhm  42564  rngcrescrhmALTV  42582
 Copyright terms: Public domain W3C validator