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

Theorem dmss 5010
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 3327 . . . 4
21eximdv 1667 . . 3
3 vex 2954 . . . 4
43eldm2 5009 . . 3
53eldm2 5009 . . 3
62, 4, 53imtr4g 264 . 2
76ssrdv 3339 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  E.wex 1581  e.wcel 1749  C_wss 3305  <.cop 3856  domcdm 4811
This theorem is referenced by:  dmeq  5011  dmv  5026  rnss  5039  dmiin  5054  ssxpb  5244  sofld  5258  relrelss  5333  funssxp  5541  fndmdif  5777  fneqeql2  5782  dff3  5826  frxp  6651  fnwelem  6656  tposss  6708  smores  6772  smores2  6774  tfrlem13  6808  imafi  7563  hartogslem1  7703  wemapso  7712  r0weon  8126  infxpenlem  8127  brdom3  8642  brdom5  8643  brdom4  8644  fpwwe2lem13  8755  fpwwe2  8756  canth4  8760  canthwelem  8763  pwfseqlem4  8775  nqerf  9045  dmrecnq  9083  uzrdgfni  11722  rlimpm  12919  isstruct2  14123  strlemor1  14205  strleun  14208  imasaddfnlem  14406  imasvscafn  14415  isohom  14650  catcoppccl  14916  tsrss  15333  ledm  15334  dirdm  15344  f1omvdmvd  15886  mvdco  15888  f1omvdconj  15889  pmtrfb  15908  pmtrfconj  15909  symggen  15913  symggen2  15914  pmtrdifellem1  15919  pmtrdifellem2  15920  psgnunilem1  15936  gsum2d  16355  lspextmo  16946  psgnghm2  17719  dsmmfi  17871  lindfres  17951  mdet1  18110  tsmsxp  19429  ustssco  19489  setsmstopn  19753  metustexhalfOLD  19838  metustexhalf  19839  tngtopn  19936  equivcau  20511  cmetss  20525  dvbssntr  21075  pserdv  21635  uhgrares  22921  umgrares  22937  usgrares  22967  hlimcaui  24318  metideq  26029  fundmpss  27279  wfrlem16  27441  fixssdm  27639  filnetlem3  28272  filnetlem4  28273  ssbnd  28358  bnd2lem  28361  ismrcd1  28706  istopclsd  28708  gsumX2d  30504
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-rab 2703  df-v 2953  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-sn 3859  df-pr 3860  df-op 3862  df-br 4268  df-dm 4821
  Copyright terms: Public domain W3C validator