Theorem dmeqd 5326

Description: Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)

Hypothesis

Ref	Expression
dmeqd.1	|- ( ph -> A = B )

Assertion

Ref	Expression
dmeqd	|- ( ph -> dom A = dom B )

Proof of Theorem dmeqd

Step	Hyp	Ref	Expression
1		dmeqd.1	. 2 |- ( ph -> A = B )
2		dmeq 5324	. 2 |- ( A = B -> dom A = dom B )
3	1, 2	syl 17	1 |- ( ph -> dom A = dom B )

Syntax hints:   -> wi 4   = wceq 1483   dom cdm 5114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-dm 5124

This theorem is referenced by:  dmxpid  5345  rneq  5351  dmxpss  5565  dmsnopss  5607  dmsnsnsn  5613  f10d  6170  fndmin  6324  fninfp  6440  fndifnfp  6442  ovmpt3rabdm  6892  elxp4  7110  1stval  7170  fo1st  7188  f1stres  7190  bropopvvv  7255  bropfvvvv  7257  suppsnop  7309  mpt2curryd  7395  errn  7764  xpassen  8054  xpdom2  8055  oicl  8434  oif  8435  hartogslem1  8447  cantnfdm  8561  cantnfval  8565  cantnf0  8572  cantnfres  8574  cnfcomlem  8596  hsmexlem4  9251  hsmexlem5  9252  axdc3lem2  9273  ttukeylem3  9333  hashfun  13224  s1dmALT  13389  swrdval  13417  swrd0  13434  s2dmALT  13653  s4dom  13664  dmtrclfv  13759  relexpnndm  13781  relexpdmg  13782  relexpnnrn  13785  relexpfld  13789  relexpaddg  13793  shftdm  13811  rlim  14226  ramval  15712  isstruct2  15867  setsvalg  15887  setsdm  15892  prdsval  16115  homfeqbas  16356  invf  16428  dfiso2  16432  oppciso  16441  cicsym  16464  sscfn1  16477  sscfn2  16478  isssc  16480  rescval  16487  rescval2  16488  issubc  16495  issubc2  16496  cofuval  16542  resfval  16552  resfval2  16553  resf1st  16554  estrreslem2  16778  prfval  16839  lubdm  16979  glbdm  16992  joindm  17003  meetdm  17017  islat  17047  isclat  17109  oduclatb  17144  gsumvalx  17270  cntzrcl  17760  f1omvdco2  17868  pmtrfrn  17878  symgsssg  17887  symgfisg  17888  symggen  17890  pmtrdifwrdellem3  17903  pmtrdifwrdel2lem1  17904  pmtrdifwrdel  17905  pmtrdifwrdel2  17906  psgnunilem1  17913  psgnunilem5  17914  psgnunilem2  17915  psgnunilem3  17916  psgneldm  17923  dmdprd  18397  dprdval  18402  dpjfval  18454  ablfaclem3  18486  mpfrcl  19518  zrhcofipsgn  19939  elocv  20012  ishil  20062  dsmmval  20078  mamudm  20194  mavmuldm  20356  mavmul0g  20359  m1detdiag  20403  decpmatval0  20569  decpmatval  20570  pmatcollpw3lem  20588  iscnp2  21043  ptval  21373  ptcmplem2  21857  cnextfval  21866  tsmsval2  21933  ustbas2  22029  utopval  22036  tusval  22070  ucnval  22081  iscfilu  22092  psmetdmdm  22110  xmetdmdm  22140  blfvalps  22188  setsmstopn  22283  tmsval  22286  metuval  22354  tngtopn  22454  cfilfval  23062  caufval  23073  limcfval  23636  dvfval  23661  dvbsss  23666  perfdvf  23667  dvn2bss  23693  dvnres  23694  dvcmul  23707  dvcmulf  23708  dvcj  23713  dvnfre  23715  dvexp  23716  dvmptres3  23719  dvmptcl  23722  dvmptadd  23723  dvmptmul  23724  dvmptres2  23725  dvmptcmul  23727  dvmptcj  23731  dvmptco  23735  rolle  23753  cmvth  23754  mvth  23755  dvlip  23756  dvlipcn  23757  dvlip2  23758  c1liplem1  23759  dveq0  23763  dv11cn  23764  dvle  23770  dvivthlem1  23771  dvivth  23773  dvne0  23774  lhop1lem  23776  lhop2  23778  lhop  23779  dvcnvrelem1  23780  dvcvx  23783  dvfsumle  23784  dvfsumge  23785  dvfsumabs  23786  dvmptrecl  23787  dvfsumlem2  23790  itgsubstlem  23811  taylfval  24113  tayl0  24116  dvtaylp  24124  dvntaylp  24125  dvntaylp0  24126  taylthlem1  24127  taylthlem2  24128  ulmdvlem1  24154  pserdv  24183  pige3  24269  logtayl  24406  relogbf  24529  lgamgulmlem2  24756  perpln1  25605  isuhgr  25955  isushgr  25956  uhgreq12g  25960  isuhgrop  25965  uhgrun  25969  uhgrstrrepe  25973  isupgr  25979  upgrop  25989  isumgr  25990  upgr1e  26008  upgrun  26013  umgrun  26015  isuspgr  26047  isusgr  26048  isuspgrop  26056  isusgrop  26057  ausgrusgrb  26060  usgrstrrepe  26127  uspgr1e  26136  usgrexmpl  26155  issubgr  26163  uhgrspansubgrlem  26182  usgrexi  26337  vtxdgfval  26363  vtxdeqd  26373  vtxdun  26377  1loopgrvd0  26400  1hevtxdg0  26401  1hevtxdg1  26402  umgr2v2e  26421  umgr2v2evd2  26423  ewlksfval  26497  wksfval  26505  wlkres  26567  wlkp1  26578  eupths  27060  eupthres  27075  trlsegvdeglem4  27083  trlsegvdeglem5  27084  grporndm  27364  hmoval  27665  smatrcl  29862  metidval  29933  pstmval  29938  prsssdm  29963  ordtrestNEW  29967  ofcfval  30160  ofcfval3  30164  brae  30304  braew  30305  faeval  30309  mbfmcst  30321  carsgval  30365  issibf  30395  sitmval  30411  0rrv  30513  dstrvprob  30533  nosupdm  31850  nosupbday  31851  nosupres  31853  nosupbnd1lem1  31854  nosupbnd1  31860  nosupbnd2  31862  cnndvlem2  32529  bj-finsumval0  33147  cureq  33385  curf  33387  curunc  33391  sdclem2  33538  ismtyval  33599  isass  33645  isexid  33646  ismndo2  33673  exidreslem  33676  rngodm1dm2  33731  divrngcl  33756  isdrngo2  33757  isopos  34467  isatl  34586  dibffval  36429  dibfval  36430  conrel2d  37956  iunrelexp0  37994  dmtrclfvRP  38022  rntrclfvRP  38023  neicvgbex  38410  dvsconst  38529  expgrowth  38534  fnlimfvre  39906  dvsinax  40127  dvmptresicc  40134  dvcosax  40141  dvbdfbdioolem1  40143  itgsinexplem1  40169  itgcoscmulx  40185  dirkeritg  40319  dirkercncflem2  40321  fourierdlem60  40383  fourierdlem61  40384  fourierdlem74  40397  fourierdlem75  40398  fourierdlem80  40403  fourierdlem94  40417  fourierdlem103  40426  fourierdlem104  40427  fourierdlem113  40436  dmvon  40820  ovnovollem1  40870  smflimlem3  40981  smflimlem4  40982  smflim  40985  smflim2  41012  smfpimcc  41014  smflimmpt  41016  smfsuplem2  41018  smfsuplem3  41019  smfsup  41020  smfsupmpt  41021  smfinflem  41023  smfinf  41024  smfinfmpt  41025  smflimsuplem1  41026  smflimsuplem2  41027  smflimsuplem3  41028  smflimsuplem4  41029  smflimsuplem7  41032  smflimsup  41034  smflimsupmpt  41035  smfliminf  41037  smfliminfmpt  41038  dfateq12d  41209  upwlksfval  41716  mndpsuppss  42152