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

Theorem xpss12 5148
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 3562 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
2 ssel 3562 . . . 4 (𝐶𝐷 → (𝑦𝐶𝑦𝐷))
31, 2im2anan9 876 . . 3 ((𝐴𝐵𝐶𝐷) → ((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐷)))
43ssopab2dv 4929 . 2 ((𝐴𝐵𝐶𝐷) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐷)})
5 df-xp 5044 . 2 (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)}
6 df-xp 5044 . 2 (𝐵 × 𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐷)}
74, 5, 63sstr4g 3609 1 ((𝐴𝐵𝐶𝐷) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 1977  wss 3540  {copab 4642   × cxp 5036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-in 3547  df-ss 3554  df-opab 4644  df-xp 5044
This theorem is referenced by:  xpss  5149  xpss1  5151  xpss2  5152  djussxp  5189  ssxpb  5487  ssrnres  5491  cossxp  5575  relrelss  5576  fssxp  5973  oprabss  6644  oprres  6700  pmss12g  7770  marypha1lem  8222  marypha2lem1  8224  hartogslem1  8330  infxpenlem  8719  dfac5lem4  8832  axdc4lem  9160  fpwwe2lem1  9332  fpwwe2lem11  9341  fpwwe2lem12  9342  fpwwe2lem13  9343  canthwe  9352  tskxpss  9473  dmaddpi  9591  dmmulpi  9592  addnqf  9649  mulnqf  9650  rexpssxrxp  9963  ltrelxr  9978  mulnzcnopr  10552  dfz2  11272  elq  11666  leiso  13100  znnen  14780  eucalg  15138  phimullem  15322  imasless  16023  sscpwex  16298  fullsubc  16333  fullresc  16334  wunfunc  16382  funcres2c  16384  homaf  16503  dmcoass  16539  catcoppccl  16581  catcfuccl  16582  catcxpccl  16670  znleval  19722  txuni2  21178  txbas  21180  txcld  21216  txcls  21217  neitx  21220  txcnp  21233  txlly  21249  txnlly  21250  hausdiag  21258  tx1stc  21263  txkgen  21265  xkococnlem  21272  cnmpt2res  21290  clssubg  21722  tsmsxplem1  21766  tsmsxplem2  21767  tsmsxp  21768  trust  21843  ustuqtop1  21855  psmetres2  21929  xmetres2  21976  metres2  21978  ressprdsds  21986  xmetresbl  22052  ressxms  22140  metustexhalf  22171  cfilucfil  22174  restmetu  22185  nrginvrcn  22306  qtopbaslem  22372  tgqioo  22411  re2ndc  22412  resubmet  22413  xrsdsre  22421  bndth  22565  lebnumii  22573  iscfil2  22872  cmsss  22955  minveclem3a  23006  ovolfsf  23047  opnmblALT  23177  mbfimaopnlem  23228  itg1addlem4  23272  limccnp2  23462  taylfval  23917  taylf  23919  dvdsmulf1o  24720  fsumdvdsmul  24721  sspg  26967  ssps  26969  sspmlem  26971  issh2  27450  hhssabloilem  27502  hhssabloi  27503  hhssnv  27505  hhshsslem1  27508  shsel  27557  ofrn2  28822  gtiso  28861  xrofsup  28923  fimaproj  29228  txomap  29229  tpr2rico  29286  prsss  29290  raddcn  29303  xrge0pluscn  29314  br2base  29658  dya2iocnrect  29670  dya2iocucvr  29673  eulerpartlemgh  29767  eulerpartlemgs2  29769  cvmlift2lem9  30547  cvmlift2lem10  30548  cvmlift2lem11  30549  cvmlift2lem12  30550  mpstssv  30690  elxp8  32395  mblfinlem2  32617  ftc1anc  32663  ssbnd  32757  prdsbnd2  32764  cnpwstotbnd  32766  reheibor  32808  exidreslem  32846  divrngcl  32926  isdrngo2  32927  dibss  35476  arearect  36820  rtrclex  36943  rtrclexi  36947  rp-imass  37085  idhe  37101  rr2sscn2  38523  fourierdlem42  39042  opnvonmbllem2  39523  rnghmresfn  41755  rnghmsscmap2  41765  rnghmsscmap  41766  rhmresfn  41801  rhmsscmap2  41811  rhmsscmap  41812  rhmsscrnghm  41818  rngcrescrhm  41877  rngcrescrhmALTV  41896
  Copyright terms: Public domain W3C validator