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

Theorem xpss12 5568
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 3964 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
2 ssel 3964 . . . 4 (𝐶𝐷 → (𝑦𝐶𝑦𝐷))
31, 2im2anan9 619 . . 3 ((𝐴𝐵𝐶𝐷) → ((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐷)))
43ssopab2dv 5434 . 2 ((𝐴𝐵𝐶𝐷) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐷)})
5 df-xp 5559 . 2 (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)}
6 df-xp 5559 . 2 (𝐵 × 𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐷)}
74, 5, 63sstr4g 4015 1 ((𝐴𝐵𝐶𝐷) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2107  wss 3939  {copab 5124   × cxp 5551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-in 3946  df-ss 3955  df-opab 5125  df-xp 5559
This theorem is referenced by:  xpss  5569  inxpssres  5570  xpss1  5572  xpss2  5573  djussxp  5714  ssxpb  6028  cossxp  6120  relrelss  6121  fssxp  6530  oprabss  7253  oprres  7309  fimaproj  7823  pmss12g  8426  marypha1lem  8889  marypha2lem1  8891  hartogslem1  8998  infxpenlem  9431  dfac5lem4  9544  axdc4lem  9869  fpwwe2lem1  10045  fpwwe2lem11  10054  fpwwe2lem12  10055  fpwwe2lem13  10056  canthwe  10065  tskxpss  10186  dmaddpi  10304  dmmulpi  10305  addnqf  10362  mulnqf  10363  rexpssxrxp  10678  ltrelxr  10694  mulnzcnopr  11278  dfz2  11992  elq  12342  leiso  13810  znnen  15557  phimullem  16108  imasless  16805  sscpwex  17077  fullsubc  17112  fullresc  17113  wunfunc  17161  funcres2c  17163  homaf  17282  dmcoass  17318  catcoppccl  17360  catcfuccl  17361  catcxpccl  17449  znleval  20619  txuni2  22091  txbas  22093  txcld  22129  txcls  22130  neitx  22133  txcnp  22146  txlly  22162  txnlly  22163  hausdiag  22171  tx1stc  22176  txkgen  22178  xkococnlem  22185  cnmpt2res  22203  clssubg  22634  tsmsxplem1  22678  tsmsxplem2  22679  tsmsxp  22680  trust  22755  ustuqtop1  22767  psmetres2  22841  xmetres2  22888  metres2  22890  ressprdsds  22898  xmetresbl  22964  ressxms  23052  metustexhalf  23083  cfilucfil  23086  restmetu  23097  nrginvrcn  23218  qtopbaslem  23284  tgqioo  23325  re2ndc  23326  resubmet  23327  xrsdsre  23335  bndth  23479  lebnumii  23487  iscfil2  23786  cmssmscld  23870  cmsss  23871  cmscsscms  23893  minveclem3a  23947  ovolfsf  23989  opnmblALT  24121  mbfimaopnlem  24173  itg1addlem4  24217  limccnp2  24407  taylfval  24864  taylf  24866  dvdsmulf1o  25687  fsumdvdsmul  25688  sspg  28421  ssps  28423  sspmlem  28425  issh2  28902  hhssabloilem  28954  hhssabloi  28955  hhssnv  28957  hhshsslem1  28960  shsel  29007  ofrn2  30304  gtiso  30351  xrofsup  30407  txomap  30986  tpr2rico  31043  prsss  31047  raddcn  31060  xrge0pluscn  31071  br2base  31415  dya2iocnrect  31427  dya2iocucvr  31430  eulerpartlemgh  31524  eulerpartlemgs2  31526  cvmlift2lem9  32444  cvmlift2lem10  32445  cvmlift2lem11  32446  cvmlift2lem12  32447  mpstssv  32672  elxp8  34523  mblfinlem2  34799  ftc1anc  34844  ssbnd  34936  prdsbnd2  34943  cnpwstotbnd  34945  reheibor  34987  exidreslem  35025  divrngcl  35105  isdrngo2  35106  dibss  38174  xppss12  38982  arearect  39689  rtrclex  39844  rtrclexi  39848  rp-imass  39984  rr2sscn2  41501  fourierdlem42  42302  opnvonmbllem2  42783  rnghmresfn  44068  rnghmsscmap2  44078  rnghmsscmap  44079  rhmresfn  44114  rhmsscmap2  44124  rhmsscmap  44125  rhmsscrnghm  44131  rngcrescrhm  44190  rngcrescrhmALTV  44208
  Copyright terms: Public domain W3C validator