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

Theorem dmeqd 5524
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 5522 . 2 (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
31, 2syl 17 1 (𝜑 → dom 𝐴 = dom 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  dom cdm 5308
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-rab 3104  df-v 3392  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-nul 4114  df-if 4277  df-sn 4368  df-pr 4370  df-op 4374  df-br 4841  df-dm 5318
This theorem is referenced by:  dmxpid  5543  rneq  5549  dmxpss  5773  dmsnopss  5816  dmsnsnsn  5822  f10d  6383  fndmin  6543  fninfp  6662  fndifnfp  6664  ovmpt3rabdm  7119  elxp4  7337  1stval  7397  fo1st  7415  f1stres  7419  bropopvvv  7486  bropfvvvv  7488  suppsnop  7540  mpt2curryd  7627  errn  7998  xpassen  8290  xpdom2  8291  oicl  8670  oif  8671  hartogslem1  8683  cantnfdm  8805  cantnfval  8809  cantnf0  8816  cantnfres  8818  cnfcomlem  8840  hsmexlem4  9533  hsmexlem5  9534  axdc3lem2  9555  ttukeylem3  9615  hashfun  13437  s1dmALT  13600  swrdval  13636  swrd0  13654  s2dmALT  13873  s4dom  13884  dmtrclfv  13978  relexpnndm  14000  relexpdmg  14001  relexpnnrn  14004  relexpfld  14008  relexpaddg  14012  shftdm  14030  rlim  14445  ramval  15925  isstruct2  16074  setsvalg  16094  setsdm  16099  prdsval  16316  homfeqbas  16556  invf  16628  dfiso2  16632  oppciso  16641  cicsym  16664  sscfn1  16677  sscfn2  16678  isssc  16680  rescval  16687  rescval2  16688  issubc  16695  issubc2  16696  cofuval  16742  resfval  16752  resfval2  16753  resf1st  16754  estrreslem2  16978  prfval  17040  lubdm  17180  glbdm  17193  joindm  17204  meetdm  17218  islat  17248  isclat  17310  oduclatb  17345  gsumvalx  17471  cntzrcl  17957  f1omvdco2  18065  pmtrfrn  18075  symgsssg  18084  symgfisg  18085  symggen  18087  pmtrdifwrdellem3  18100  pmtrdifwrdel2lem1  18101  pmtrdifwrdel  18102  pmtrdifwrdel2  18103  psgnunilem1  18110  psgnunilem5  18111  psgnunilem2  18112  psgnunilem3  18113  psgneldm  18120  dmdprd  18595  dprdval  18600  dpjfval  18652  ablfaclem3  18684  mpfrcl  19722  cofipsgn  20142  zrhcofipsgnOLD  20143  elocv  20218  ishil  20268  dsmmval  20284  mamudm  20400  mavmuldm  20563  mavmul0g  20566  m1detdiag  20610  decpmatval0  20778  decpmatval  20779  pmatcollpw3lem  20797  iscnp2  21253  ptval  21583  ptcmplem2  22066  cnextfval  22075  tsmsval2  22142  ustbas2  22238  utopval  22245  tusval  22279  ucnval  22290  iscfilu  22301  psmetdmdm  22319  xmetdmdm  22349  blfvalps  22397  setsmstopn  22492  tmsval  22495  metuval  22563  tngtopn  22663  cfilfval  23270  caufval  23281  limcfval  23846  dvfval  23871  dvbsss  23876  perfdvf  23877  dvn2bss  23903  dvnres  23904  dvcmul  23917  dvcmulf  23918  dvcj  23923  dvnfre  23925  dvexp  23926  dvmptres3  23929  dvmptcl  23932  dvmptadd  23933  dvmptmul  23934  dvmptres2  23935  dvmptcmul  23937  dvmptcj  23941  dvmptco  23945  rolle  23963  cmvth  23964  mvth  23965  dvlip  23966  dvlipcn  23967  dvlip2  23968  c1liplem1  23969  dveq0  23973  dv11cn  23974  dvle  23980  dvivthlem1  23981  dvivth  23983  dvne0  23984  lhop1lem  23986  lhop2  23988  lhop  23989  dvcnvrelem1  23990  dvcvx  23993  dvfsumle  23994  dvfsumge  23995  dvfsumabs  23996  dvmptrecl  23997  dvfsumlem2  24000  itgsubstlem  24021  taylfval  24323  tayl0  24326  dvtaylp  24334  dvntaylp  24335  dvntaylp0  24336  taylthlem1  24337  taylthlem2  24338  ulmdvlem1  24364  pserdv  24393  pige3  24480  logtayl  24616  relogbf  24739  lgamgulmlem2  24966  perpln1  25815  isuhgr  26165  isushgr  26166  uhgreq12g  26170  isuhgrop  26175  uhgrun  26179  uhgrstrrepe  26183  isupgr  26189  upgrop  26199  isumgr  26200  upgr1e  26218  upgrun  26223  umgrun  26225  isuspgr  26258  isusgr  26259  isuspgrop  26267  isusgrop  26268  ausgrusgrb  26271  usgrstrrepe  26339  uspgr1e  26348  usgrexmpl  26367  issubgr  26375  uhgrspansubgrlem  26394  usgrexi  26561  vtxdgfval  26587  vtxdeqd  26597  vtxdun  26601  1loopgrvd0  26624  1hevtxdg0  26625  1hevtxdg1  26626  umgr2v2e  26645  umgr2v2evd2  26647  ewlksfval  26721  wksfval  26729  wlkres  26791  wlkp1  26802  eupths  27369  eupthres  27384  trlsegvdeglem4  27392  trlsegvdeglem5  27393  grporndm  27689  hmoval  27990  smatrcl  30184  metidval  30255  pstmval  30260  prsssdm  30285  ordtrestNEW  30289  ofcfval  30482  ofcfval3  30486  brae  30626  braew  30627  faeval  30631  mbfmcst  30643  carsgval  30687  issibf  30717  sitmval  30733  0rrv  30835  dstrvprob  30855  nosupdm  32168  nosupbday  32169  nosupres  32171  nosupbnd1lem1  32172  nosupbnd1  32178  nosupbnd2  32180  cnndvlem2  32843  bj-finsumval0  33461  cureq  33695  curf  33697  curunc  33701  sdclem2  33846  ismtyval  33907  isass  33953  isexid  33954  ismndo2  33981  exidreslem  33984  rngodm1dm2  34039  divrngcl  34064  isdrngo2  34065  isopos  34957  isatl  35076  dibffval  36918  dibfval  36919  conrel2d  38453  iunrelexp0  38491  dmtrclfvRP  38519  rntrclfvRP  38520  neicvgbex  38907  dvsconst  39026  expgrowth  39031  fnlimfvre  40383  dvsinax  40604  dvmptresicc  40611  dvcosax  40618  dvbdfbdioolem1  40620  itgsinexplem1  40646  itgcoscmulx  40661  dirkeritg  40795  dirkercncflem2  40797  fourierdlem60  40859  fourierdlem61  40860  fourierdlem74  40873  fourierdlem75  40874  fourierdlem80  40879  fourierdlem94  40893  fourierdlem103  40902  fourierdlem104  40903  fourierdlem113  40912  dmvon  41299  ovnovollem1  41349  smflimlem3  41460  smflimlem4  41461  smflim  41464  smflim2  41491  smfpimcc  41493  smflimmpt  41495  smfsuplem2  41497  smfsuplem3  41498  smfsup  41499  smfsupmpt  41500  smfinflem  41502  smfinf  41503  smfinfmpt  41504  smflimsuplem1  41505  smflimsuplem2  41506  smflimsuplem3  41507  smflimsuplem4  41508  smflimsuplem7  41511  smflimsup  41513  smflimsupmpt  41514  smfliminf  41516  smfliminfmpt  41517  dfateq12d  41712  upwlksfval  42281  mndpsuppss  42717
  Copyright terms: Public domain W3C validator