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

Theorem dmss 5207
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 3497 . . . 4
21eximdv 1710 . . 3
3 vex 3112 . . . 4
43eldm2 5206 . . 3
53eldm2 5206 . . 3
62, 4, 53imtr4g 270 . 2
76ssrdv 3509 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  E.wex 1612  e.wcel 1818  C_wss 3475  <.cop 4035  domcdm 5004
This theorem is referenced by:  dmeq  5208  dmv  5223  rnss  5236  dmiin  5251  ssxpb  5446  sofld  5460  relrelss  5536  funssxp  5749  fndmdif  5991  fneqeql2  5996  dff3  6044  frxp  6910  fnwelem  6915  funsssuppss  6945  tposss  6975  smores  7042  smores2  7044  tfrlem13  7078  imafi  7833  hartogslem1  7988  wemapso  7997  r0weon  8411  infxpenlem  8412  brdom3  8927  brdom5  8928  brdom4  8929  fpwwe2lem13  9041  fpwwe2  9042  canth4  9046  canthwelem  9049  pwfseqlem4  9061  nqerf  9329  dmrecnq  9367  uzrdgfni  12069  rlimpm  13323  isstruct2  14641  strlemor1  14724  strleun  14727  imasaddfnlem  14925  imasvscafn  14934  isohom  15166  catcoppccl  15435  tsrss  15853  ledm  15854  dirdm  15864  f1omvdmvd  16468  mvdco  16470  f1omvdconj  16471  pmtrfb  16490  pmtrfconj  16491  symggen  16495  symggen2  16496  pmtrdifellem1  16501  pmtrdifellem2  16502  psgnunilem1  16518  gsum2d  16999  gsum2dOLD  17000  lspextmo  17702  dsmmfi  18769  lindfres  18858  mdetdiaglem  19100  tsmsxp  20657  ustssco  20717  setsmstopn  20981  metustexhalfOLD  21066  metustexhalf  21067  tngtopn  21164  equivcau  21739  cmetss  21753  dvbssntr  22304  pserdv  22824  uhgrares  24308  umgrares  24324  usgrares  24369  hlimcaui  26154  metideq  27872  fundmpss  29196  wfrlem16  29358  fixssdm  29556  filnetlem3  30198  filnetlem4  30199  ssbnd  30284  bnd2lem  30287  ismrcd1  30630  istopclsd  30632  fourierdlem80  31969  uhgres  32379  rp-imass  37795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-dm 5014
  Copyright terms: Public domain W3C validator