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

Theorem xpss12 5134
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 3558 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
2 ssel 3558 . . . 4 (𝐶𝐷 → (𝑦𝐶𝑦𝐷))
31, 2im2anan9 875 . . 3 ((𝐴𝐵𝐶𝐷) → ((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐷)))
43ssopab2dv 4916 . 2 ((𝐴𝐵𝐶𝐷) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐷)})
5 df-xp 5031 . 2 (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)}
6 df-xp 5031 . 2 (𝐵 × 𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐷)}
74, 5, 63sstr4g 3605 1 ((𝐴𝐵𝐶𝐷) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  wss 3536  {copab 4633   × cxp 5023
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-in 3543  df-ss 3550  df-opab 4635  df-xp 5031
This theorem is referenced by:  xpss  5135  xpss1  5137  xpss2  5138  djussxp  5174  ssxpb  5470  ssrnres  5474  cossxp  5558  relrelss  5559  fssxp  5956  oprabss  6619  pmss12g  7744  marypha1lem  8196  marypha2lem1  8198  hartogslem1  8304  infxpenlem  8693  dfac5lem4  8806  axdc4lem  9134  fpwwe2lem1  9306  fpwwe2lem11  9315  fpwwe2lem12  9316  fpwwe2lem13  9317  canthwe  9326  tskxpss  9447  dmaddpi  9565  dmmulpi  9566  addnqf  9623  mulnqf  9624  rexpssxrxp  9937  ltrelxr  9947  mulnzcnopr  10519  dfz2  11225  elq  11619  leiso  13049  znnen  14723  eucalg  15081  phimullem  15265  imasless  15966  sscpwex  16241  fullsubc  16276  fullresc  16277  wunfunc  16325  funcres2c  16327  homaf  16446  dmcoass  16482  catcoppccl  16524  catcfuccl  16525  catcxpccl  16613  znleval  19664  txuni2  21117  txbas  21119  txcld  21155  txcls  21156  neitx  21159  txcnp  21172  txlly  21188  txnlly  21189  hausdiag  21197  tx1stc  21202  txkgen  21204  xkococnlem  21211  cnmpt2res  21229  clssubg  21661  tsmsxplem1  21705  tsmsxplem2  21706  tsmsxp  21707  trust  21782  ustuqtop1  21794  psmetres2  21868  xmetres2  21914  metres2  21916  ressprdsds  21924  xmetresbl  21990  ressxms  22078  metustexhalf  22109  cfilucfil  22112  restmetu  22123  nrginvrcn  22236  qtopbaslem  22301  tgqioo  22340  re2ndc  22341  resubmet  22342  xrsdsre  22350  bndth  22493  lebnumii  22501  iscfil2  22787  cmsss  22869  minveclem3a  22920  ovolfsf  22961  opnmblALT  23091  mbfimaopnlem  23142  itg1addlem4  23186  limccnp2  23376  taylfval  23831  taylf  23833  dvdsmulf1o  24634  fsumdvdsmul  24635  sspg  26768  ssps  26770  sspmlem  26772  issh2  27253  hhssabloilem  27305  hhssabloi  27306  hhssnv  27308  hhshsslem1  27311  shsel  27360  ofrn2  28625  gtiso  28664  xrofsup  28726  fimaproj  29031  txomap  29032  tpr2rico  29089  prsss  29093  raddcn  29106  xrge0pluscn  29117  br2base  29461  dya2iocnrect  29473  dya2iocucvr  29476  eulerpartlemgh  29570  eulerpartlemgs2  29572  cvmlift2lem9  30350  cvmlift2lem10  30351  cvmlift2lem11  30352  cvmlift2lem12  30353  mpstssv  30493  elxp8  32195  mblfinlem2  32417  ftc1anc  32463  ssbnd  32557  prdsbnd2  32564  cnpwstotbnd  32566  reheibor  32608  exidreslem  32646  divrngcl  32726  isdrngo2  32727  dibss  35276  arearect  36620  rtrclex  36743  rtrclexi  36747  rp-imass  36885  idhe  36901  rr2sscn2  38324  fourierdlem42  38843  opnvonmbllem2  39324  rnghmresfn  41754  rnghmsscmap2  41764  rnghmsscmap  41765  rhmresfn  41800  rhmsscmap2  41810  rhmsscmap  41811  rhmsscrnghm  41817  rngcrescrhm  41876  rngcrescrhmALTV  41895
  Copyright terms: Public domain W3C validator