Theorem dmeqd 5774

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

Step	Hyp	Ref	Expression
1		dmeqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		dmeq 5772	. 2 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → dom 𝐴 = dom 𝐵)

Syntax hints:   → wi 4   = wceq 1537  dom cdm 5555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-dm 5565

This theorem is referenced by:  dmxpid  5800  rneq  5806  dmxpss  6028  dmsnopss  6071  dmsnsnsn  6077  f10d  6648  fndmin  6815  fninfp  6936  fndifnfp  6938  ovmpt3rabdm  7404  elxp4  7627  1stval  7691  fo1st  7709  f1stres  7713  bropopvvv  7785  bropfvvvv  7787  mpocurryd  7935  errn  8311  xpassen  8611  xpdom2  8612  oicl  8993  oif  8994  hartogslem1  9006  cantnfdm  9127  cantnfval  9131  cantnf0  9138  cantnfres  9140  cnfcomlem  9162  hsmexlem4  9851  hsmexlem5  9852  axdc3lem2  9873  ttukeylem3  9933  hashfun  13799  s1dmALT  13963  swrdval  14005  swrd0  14020  s2dmALT  14270  s4dom  14281  dmtrclfv  14378  relexpnndm  14400  relexpdmg  14401  relexpnnrn  14404  relexpfld  14408  relexpaddg  14412  shftdm  14430  rlim  14852  ramval  16344  isstruct2  16493  setsvalg  16512  setsdm  16517  prdsval  16728  homfeqbas  16966  invf  17038  dfiso2  17042  oppciso  17051  cicsym  17074  sscfn1  17087  sscfn2  17088  isssc  17090  rescval  17097  rescval2  17098  issubc  17105  issubc2  17106  cofuval  17152  resfval  17162  resfval2  17163  resf1st  17164  estrreslem2  17388  prfval  17449  lubdm  17589  glbdm  17602  joindm  17613  meetdm  17627  islat  17657  isclat  17719  oduclatb  17754  gsumvalx  17886  cntzrcl  18457  f1omvdco2  18576  pmtrfrn  18586  symgsssg  18595  symgfisg  18596  symggen  18598  pmtrdifwrdellem3  18611  pmtrdifwrdel2lem1  18612  pmtrdifwrdel  18613  pmtrdifwrdel2  18614  psgnunilem1  18621  psgnunilem5  18622  psgnunilem2  18623  psgnunilem3  18624  psgneldm  18631  dmdprd  19120  dprdval  19125  dpjfval  19177  ablfaclem3  19209  mpfrcl  20298  cofipsgn  20737  elocv  20812  ishil  20862  dsmmval  20878  mamudm  20999  mavmuldm  21159  mavmul0g  21162  m1detdiag  21206  decpmatval0  21372  decpmatval  21373  pmatcollpw3lem  21391  iscnp2  21847  ptval  22178  ptcmplem2  22661  cnextfval  22670  tsmsval2  22738  ustbas2  22834  utopval  22841  tusval  22875  ucnval  22886  iscfilu  22897  psmetdmdm  22915  xmetdmdm  22945  blfvalps  22993  setsmstopn  23088  tmsval  23091  metuval  23159  tngtopn  23259  cfilfval  23867  caufval  23878  limcfval  24470  dvfval  24495  dvbsss  24500  perfdvf  24501  dvn2bss  24527  dvnres  24528  dvcmul  24541  dvcmulf  24542  dvcj  24547  dvnfre  24549  dvexp  24550  dvmptres3  24553  dvmptcl  24556  dvmptadd  24557  dvmptmul  24558  dvmptres2  24559  dvmptcmul  24561  dvmptcj  24565  dvmptco  24569  rolle  24587  cmvth  24588  mvth  24589  dvlip  24590  dvlipcn  24591  dvlip2  24592  c1liplem1  24593  dveq0  24597  dv11cn  24598  dvle  24604  dvivthlem1  24605  dvivth  24607  dvne0  24608  lhop1lem  24610  lhop2  24612  lhop  24613  dvcnvrelem1  24614  dvcvx  24617  dvfsumle  24618  dvfsumge  24619  dvfsumabs  24620  dvmptrecl  24621  dvfsumlem2  24624  itgsubstlem  24645  taylfval  24947  tayl0  24950  dvtaylp  24958  dvntaylp  24959  dvntaylp0  24960  taylthlem1  24961  taylthlem2  24962  ulmdvlem1  24988  pserdv  25017  pige3ALT  25105  logtayl  25243  relogbf  25369  lgamgulmlem2  25607  perpln1  26496  isuhgr  26845  isushgr  26846  uhgreq12g  26850  isuhgrop  26855  uhgrun  26859  uhgrstrrepe  26863  isupgr  26869  upgrop  26879  isumgr  26880  upgr1e  26898  upgrun  26903  umgrun  26905  isuspgr  26937  isusgr  26938  isuspgrop  26946  isusgrop  26947  ausgrusgrb  26950  usgrstrrepe  27017  uspgr1e  27026  usgrexmpl  27045  issubgr  27053  uhgrspansubgrlem  27072  usgrexi  27223  vtxdgfval  27249  vtxdeqd  27259  vtxdun  27263  1loopgrvd0  27286  1hevtxdg0  27287  1hevtxdg1  27288  umgr2v2e  27307  umgr2v2evd2  27309  ewlksfval  27383  wksfval  27391  wlkres  27452  wlkp1  27463  eupths  27979  eupthres  27994  trlsegvdeglem4  28002  trlsegvdeglem5  28003  grporndm  28287  hmoval  28587  symgcom2  30728  symgcntz  30729  pmtrcnel2  30734  cycpmco2f1  30766  cycpmrn  30785  tocyccntz  30786  smatrcl  31061  metidval  31130  pstmval  31135  prsssdm  31160  ordtrestNEW  31164  ofcfval  31357  ofcfval3  31361  brae  31500  braew  31501  faeval  31505  mbfmcst  31517  carsgval  31561  issibf  31591  sitmval  31607  0rrv  31709  dstrvprob  31729  satfdm  32616  fmlafv  32627  fmla  32628  fmlasuc0  32631  satfdmfmla  32647  nosupdm  33204  nosupbday  33205  nosupres  33207  nosupbnd1lem1  33208  nosupbnd1  33214  nosupbnd2  33216  cnndvlem2  33877  bj-finsumval0  34570  cureq  34883  curf  34885  curunc  34889  sdclem2  35032  ismtyval  35093  isass  35139  isexid  35140  ismndo2  35167  exidreslem  35170  rngodm1dm2  35225  divrngcl  35250  isdrngo2  35251  isopos  36331  isatl  36450  dibffval  38291  dibfval  38292  conrel2d  40029  iunrelexp0  40067  dmtrclfvRP  40095  rntrclfvRP  40096  neicvgbex  40482  dvsconst  40682  expgrowth  40687  fnlimfvre  41975  dvsinax  42217  dvmptresicc  42224  dvcosax  42231  dvbdfbdioolem1  42233  itgsinexplem1  42259  itgcoscmulx  42274  dirkeritg  42407  dirkercncflem2  42409  fourierdlem60  42471  fourierdlem61  42472  fourierdlem74  42485  fourierdlem75  42486  fourierdlem80  42491  fourierdlem94  42505  fourierdlem103  42514  fourierdlem104  42515  fourierdlem113  42524  dmvon  42908  ovnovollem1  42958  smflimlem3  43069  smflimlem4  43070  smflim  43073  smflim2  43100  smfpimcc  43102  smflimmpt  43104  smfsuplem2  43106  smfsuplem3  43107  smfsup  43108  smfsupmpt  43109  smfinflem  43111  smfinf  43112  smfinfmpt  43113  smflimsuplem1  43114  smflimsuplem2  43115  smflimsuplem3  43116  smflimsuplem4  43117  smflimsuplem7  43120  smflimsup  43122  smflimsupmpt  43123  smfliminf  43125  smfliminfmpt  43126  dfateq12d  43345  isomgr  44008  isomgreqve  44010  ushrisomgr  44026  upwlksfval  44030  mndpsuppss  44439