MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmss Unicode version

Theorem dmss 5156
Description: Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)
Assertion
Ref Expression
dmss

Proof of Theorem dmss
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssel 3464 . . . 4
21eximdv 1677 . . 3
3 vex 3084 . . . 4
43eldm2 5155 . . 3
53eldm2 5155 . . 3
62, 4, 53imtr4g 270 . 2
76ssrdv 3476 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  E.wex 1587  e.wcel 1758  C_wss 3442  <.cop 3999  domcdm 4957
This theorem is referenced by:  dmeq  5157  dmv  5172  rnss  5185  dmiin  5200  ssxpb  5391  sofld  5405  relrelss  5480  funssxp  5692  fndmdif  5930  fneqeql2  5935  dff3  5979  frxp  6816  fnwelem  6821  funsssuppss  6849  tposss  6880  smores  6947  smores2  6949  tfrlem13  6983  imafi  7739  hartogslem1  7893  wemapso  7902  r0weon  8316  infxpenlem  8317  brdom3  8832  brdom5  8833  brdom4  8834  fpwwe2lem13  8946  fpwwe2  8947  canth4  8951  canthwelem  8954  pwfseqlem4  8966  nqerf  9236  dmrecnq  9274  uzrdgfni  11926  rlimpm  13136  isstruct2  14341  strlemor1  14424  strleun  14427  imasaddfnlem  14625  imasvscafn  14634  isohom  14869  catcoppccl  15135  tsrss  15552  ledm  15553  dirdm  15563  f1omvdmvd  16108  mvdco  16110  f1omvdconj  16111  pmtrfb  16130  pmtrfconj  16131  symggen  16135  symggen2  16136  pmtrdifellem1  16141  pmtrdifellem2  16142  psgnunilem1  16158  gsum2d  16632  gsum2dOLD  16633  lspextmo  17313  psgnghm2  18204  dsmmfi  18356  lindfres  18445  mdetdiaglem  18672  tsmsxp  20128  ustssco  20188  setsmstopn  20452  metustexhalfOLD  20537  metustexhalf  20538  tngtopn  20635  equivcau  21210  cmetss  21224  dvbssntr  21775  pserdv  22294  uhgrares  23711  umgrares  23727  usgrares  23757  hlimcaui  25108  metideq  26777  fundmpss  28033  wfrlem16  28195  fixssdm  28393  filnetlem3  29061  filnetlem4  29062  ssbnd  29147  bnd2lem  29150  ismrcd1  29494  istopclsd  29496  fourierdlem80  30716  rp-imass  36485
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2809  df-v 3083  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-if 3906  df-sn 3994  df-pr 3996  df-op 4000  df-br 4410  df-dm 4967
  Copyright terms: Public domain W3C validator