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

Theorem dmeq 5208
Description: Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
Assertion
Ref Expression
dmeq

Proof of Theorem dmeq
StepHypRef Expression
1 dmss 5207 . . 3
2 dmss 5207 . . 3
31, 2anim12i 566 . 2
4 eqss 3518 . 2
5 eqss 3518 . 2
63, 4, 53imtr4i 266 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  C_wss 3475  domcdm 5004
This theorem is referenced by:  dmeqi  5209  dmeqd  5210  xpid11  5229  fneq1  5674  eqfnfv2  5982  nvof1o  6186  offval  6547  ofrfval  6548  offval3  6794  suppval  6920  smoeq  7040  tz7.44lem1  7090  tz7.44-2  7092  tz7.44-3  7093  ereq1  7337  fundmeng  7610  fseqenlem2  8427  dfac3  8523  dfac9  8537  dfac12lem1  8544  dfac12r  8547  ackbij2lem2  8641  ackbij2lem3  8642  r1om  8645  cfsmolem  8671  cfsmo  8672  dcomex  8848  axdc2lem  8849  axdc3lem2  8852  axdc3lem4  8854  ac7g  8875  ttukey2g  8917  s4dom  12867  ello1  13338  elo1  13349  isoval  15159  istsr  15847  islindf  18847  decpmatval0  19265  pmatcollpw3lem  19284  ordtval  19690  dfac14  20119  fmval  20444  fmf  20446  blfvalps  20886  tmsval  20984  cfilfval  21703  caufval  21714  isibl  22172  elcpn  22337  iscgrg  23904  isuhgra  24298  uhgrac  24305  uhgraeq12d  24307  isuslgra  24343  isusgra  24344  usgraeq12d  24362  wlks  24519  wlkcompim  24526  wlkelwrd  24530  ex-dm  25160  isass  25318  isexid  25319  ismgmOLD  25322  locfinreflem  27843  pstmval  27874  cntnevol  28199  omsval  28264  sitgval  28274  elprob  28348  cndprobval  28372  rrvmbfm  28381  mrsubfval  28868  relexpdm  29058  dfrtrcl2  29071  rdgprc0  29226  dfrdg2  29228  frrlem5e  29395  bdayval  29408  bdayfo  29435  nofulllem5  29466  brdomaing  29585  bpolylem  29810  bpolyval  29811  filnetlem4  30199  ismtyval  30296  aomclem6  31005  aomclem8  31007  dfac21  31012  uhg0e  32376  uhgres  32379  isfusgra  32424  fnxpdmdm  32456  bnj1385  33891  bnj1400  33894  bnj1014  34018  bnj1015  34019  bnj1326  34082  bnj1321  34083  bnj1491  34113
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