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

Theorem dmeqd 5469
Description: Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
Hypothesis
Ref Expression
dmeqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
dmeqd (𝜑 → dom 𝐴 = dom 𝐵)

Proof of Theorem dmeqd
StepHypRef Expression
1 dmeqd.1 . 2 (𝜑𝐴 = 𝐵)
2 dmeq 5467 . 2 (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
31, 2syl 17 1 (𝜑 → dom 𝐴 = dom 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1620  dom cdm 5254
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-rab 3047  df-v 3330  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316  df-br 4793  df-dm 5264
This theorem is referenced by:  dmxpid  5488  rneq  5494  dmxpss  5711  dmsnopss  5754  dmsnsnsn  5760  f10d  6319  fndmin  6475  fninfp  6592  fndifnfp  6594  ovmpt3rabdm  7045  elxp4  7263  1stval  7323  fo1st  7341  f1stres  7345  bropopvvv  7411  bropfvvvv  7413  suppsnop  7465  mpt2curryd  7552  errn  7921  xpassen  8207  xpdom2  8208  oicl  8587  oif  8588  hartogslem1  8600  cantnfdm  8722  cantnfval  8726  cantnf0  8733  cantnfres  8735  cnfcomlem  8757  hsmexlem4  9414  hsmexlem5  9415  axdc3lem2  9436  ttukeylem3  9496  hashfun  13387  s1dmALT  13551  swrdval  13587  swrd0  13605  s2dmALT  13824  s4dom  13835  dmtrclfv  13929  relexpnndm  13951  relexpdmg  13952  relexpnnrn  13955  relexpfld  13959  relexpaddg  13963  shftdm  13981  rlim  14396  ramval  15885  isstruct2  16040  setsvalg  16060  setsdm  16065  prdsval  16288  homfeqbas  16528  invf  16600  dfiso2  16604  oppciso  16613  cicsym  16636  sscfn1  16649  sscfn2  16650  isssc  16652  rescval  16659  rescval2  16660  issubc  16667  issubc2  16668  cofuval  16714  resfval  16724  resfval2  16725  resf1st  16726  estrreslem2  16950  prfval  17011  lubdm  17151  glbdm  17164  joindm  17175  meetdm  17189  islat  17219  isclat  17281  oduclatb  17316  gsumvalx  17442  cntzrcl  17931  f1omvdco2  18039  pmtrfrn  18049  symgsssg  18058  symgfisg  18059  symggen  18061  pmtrdifwrdellem3  18074  pmtrdifwrdel2lem1  18075  pmtrdifwrdel  18076  pmtrdifwrdel2  18077  psgnunilem1  18084  psgnunilem5  18085  psgnunilem2  18086  psgnunilem3  18087  psgneldm  18094  dmdprd  18568  dprdval  18573  dpjfval  18625  ablfaclem3  18657  mpfrcl  19691  zrhcofipsgn  20112  elocv  20185  ishil  20235  dsmmval  20251  mamudm  20367  mavmuldm  20529  mavmul0g  20532  m1detdiag  20576  decpmatval0  20742  decpmatval  20743  pmatcollpw3lem  20761  iscnp2  21216  ptval  21546  ptcmplem2  22029  cnextfval  22038  tsmsval2  22105  ustbas2  22201  utopval  22208  tusval  22242  ucnval  22253  iscfilu  22264  psmetdmdm  22282  xmetdmdm  22312  blfvalps  22360  setsmstopn  22455  tmsval  22458  metuval  22526  tngtopn  22626  cfilfval  23233  caufval  23244  limcfval  23806  dvfval  23831  dvbsss  23836  perfdvf  23837  dvn2bss  23863  dvnres  23864  dvcmul  23877  dvcmulf  23878  dvcj  23883  dvnfre  23885  dvexp  23886  dvmptres3  23889  dvmptcl  23892  dvmptadd  23893  dvmptmul  23894  dvmptres2  23895  dvmptcmul  23897  dvmptcj  23901  dvmptco  23905  rolle  23923  cmvth  23924  mvth  23925  dvlip  23926  dvlipcn  23927  dvlip2  23928  c1liplem1  23929  dveq0  23933  dv11cn  23934  dvle  23940  dvivthlem1  23941  dvivth  23943  dvne0  23944  lhop1lem  23946  lhop2  23948  lhop  23949  dvcnvrelem1  23950  dvcvx  23953  dvfsumle  23954  dvfsumge  23955  dvfsumabs  23956  dvmptrecl  23957  dvfsumlem2  23960  itgsubstlem  23981  taylfval  24283  tayl0  24286  dvtaylp  24294  dvntaylp  24295  dvntaylp0  24296  taylthlem1  24297  taylthlem2  24298  ulmdvlem1  24324  pserdv  24353  pige3  24439  logtayl  24576  relogbf  24699  lgamgulmlem2  24926  perpln1  25775  isuhgr  26125  isushgr  26126  uhgreq12g  26130  isuhgrop  26135  uhgrun  26139  uhgrstrrepe  26143  isupgr  26149  upgrop  26159  isumgr  26160  upgr1e  26178  upgrun  26183  umgrun  26185  isuspgr  26217  isusgr  26218  isuspgrop  26226  isusgrop  26227  ausgrusgrb  26230  usgrstrrepe  26297  uspgr1e  26306  usgrexmpl  26325  issubgr  26333  uhgrspansubgrlem  26352  usgrexi  26518  vtxdgfval  26544  vtxdeqd  26554  vtxdun  26558  1loopgrvd0  26581  1hevtxdg0  26582  1hevtxdg1  26583  umgr2v2e  26602  umgr2v2evd2  26604  ewlksfval  26678  wksfval  26686  wlkres  26748  wlkp1  26759  eupths  27323  eupthres  27338  trlsegvdeglem4  27346  trlsegvdeglem5  27347  grporndm  27644  hmoval  27945  smatrcl  30142  metidval  30213  pstmval  30218  prsssdm  30243  ordtrestNEW  30247  ofcfval  30440  ofcfval3  30444  brae  30584  braew  30585  faeval  30589  mbfmcst  30601  carsgval  30645  issibf  30675  sitmval  30691  0rrv  30793  dstrvprob  30813  nosupdm  32127  nosupbday  32128  nosupres  32130  nosupbnd1lem1  32131  nosupbnd1  32137  nosupbnd2  32139  cnndvlem2  32806  bj-finsumval0  33429  cureq  33667  curf  33669  curunc  33673  sdclem2  33820  ismtyval  33881  isass  33927  isexid  33928  ismndo2  33955  exidreslem  33958  rngodm1dm2  34013  divrngcl  34038  isdrngo2  34039  isopos  34939  isatl  35058  dibffval  36900  dibfval  36901  conrel2d  38427  iunrelexp0  38465  dmtrclfvRP  38493  rntrclfvRP  38494  neicvgbex  38881  dvsconst  39000  expgrowth  39005  fnlimfvre  40378  dvsinax  40599  dvmptresicc  40606  dvcosax  40613  dvbdfbdioolem1  40615  itgsinexplem1  40641  itgcoscmulx  40657  dirkeritg  40791  dirkercncflem2  40793  fourierdlem60  40855  fourierdlem61  40856  fourierdlem74  40869  fourierdlem75  40870  fourierdlem80  40875  fourierdlem94  40889  fourierdlem103  40898  fourierdlem104  40899  fourierdlem113  40908  dmvon  41295  ovnovollem1  41345  smflimlem3  41456  smflimlem4  41457  smflim  41460  smflim2  41487  smfpimcc  41489  smflimmpt  41491  smfsuplem2  41493  smfsuplem3  41494  smfsup  41495  smfsupmpt  41496  smfinflem  41498  smfinf  41499  smfinfmpt  41500  smflimsuplem1  41501  smflimsuplem2  41502  smflimsuplem3  41503  smflimsuplem4  41504  smflimsuplem7  41507  smflimsup  41509  smflimsupmpt  41510  smfliminf  41512  smfliminfmpt  41513  dfateq12d  41684  upwlksfval  42195  mndpsuppss  42631
  Copyright terms: Public domain W3C validator