Theorem dmeqi 5907

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

Hypothesis

Ref	Expression
dmeqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
dmeqi	⊢ dom 𝐴 = dom 𝐵

Proof of Theorem dmeqi

Step	Hyp	Ref	Expression
1		dmeqi.1	. 2 ⊢ 𝐴 = 𝐵
2		dmeq 5906	. 2 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
3	1, 2	ax-mp 5	1 ⊢ dom 𝐴 = dom 𝐵

Syntax hints:   = wceq 1534  dom cdm 5678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5149  df-dm 5688

This theorem is referenced by:  dmxp  5931  dmxpin  5933  rncoss  5975  rncoeq  5978  rnun  6150  rnin  6151  rnxp  6174  rnxpss  6176  imainrect  6185  dmpropg  6219  dmtpop  6222  rnsnopg  6225  fntpg  6613  opabiotadm  6980  dffv2  6993  fvopab4ndm  7035  fnreseql  7057  dmoprab  7522  reldmmpo  7555  mpondm0  7661  elmpocl  7662  opabn1stprc  8062  bropopvvv  8095  bropfvvvv  8097  frrlem7  8297  frrlem14  8304  wfrdmssOLD  8335  wfrdmclOLD  8337  wfrlem16OLD  8344  tfrlem8  8404  tfr1a  8414  tfr2a  8415  tfr2b  8416  rdgseg  8442  xpassen  9090  sbthlem5  9111  hartogslem1  9565  dmttrcl  9744  r1funlim  9789  r1sucg  9792  r1limg  9794  rankf  9817  hsmexlem4  10452  axdc2lem  10471  dmaddpi  10913  dmmulpi  10914  dmaddsr  11108  dmmulsr  11109  axaddf  11168  axmulf  11169  divsfval  17528  mvdco  19399  symgsssg  19421  symgfisg  19422  pmtrdifellem2  19431  psgnunilem5  19448  ismbl  25454  volres  25456  efcvx  26385  dvrelog  26570  dvlog  26584  nosupcbv  27634  noinfcbv  27649  noetasuplem4  27668  noetainflem4  27672  dmscut  27743  structiedg0val  28834  snstriedgval  28850  isuhgr  28872  isushgr  28873  isupgr  28896  isumgr  28907  isuspgr  28964  isusgr  28965  ushgredgedg  29041  ushgredgedgloop  29043  lfuhgr1v0e  29066  issubgr  29083  subgruhgredgd  29096  subumgredg2  29097  vtxdgfval  29280  vtxdlfgrval  29298  vtxdginducedm1lem2  29353  vtxdginducedm1fi  29357  finsumvtxdg2ssteplem4  29361  finsumvtxdg2size  29363  wlk2v2elem1  29964  dfhnorm2  30931  hlimcaui  31045  hhshsslem1  31076  dmadjss  31696  adjeu  31698  adj1o  31703  gsummpt2co  32762  cycpmrn  32864  tocyccntz  32865  prsdm  33515  mbfmcst  33879  eulerpartlemt  33991  0rrv  34071  coinflipspace  34100  bnj96  34496  bnj1398  34665  bnj1416  34670  bnj1450  34681  bnj1498  34692  bnj1501  34698  fmla  34991  fmla0  34992  gonan0  35002  satffunlem2lem2  35016  fixun  35505  linedegen  35739  matunitlindf  37091  ssbnd  37261  ismgmOLD  37323  exidreslem  37350  n0el2  37805  dmcoss3  37925  dmcoels  37929  dmmzp  42153  cnvrcl0  43055  dvsid  43768  dvsef  43769  dvsinax  45301  fperdvper  45307  dvcosax  45314  stoweidlem27  45415  fourierdlem57  45551  fourierdlem58  45552  fourierdlem62  45556  fourierdlem80  45574  fourierdlem94  45588  fourierdlem97  45591  fourierdlem113  45607  fouriersw  45619  fouriercn  45620  subsaliuncllem  45745  0ome  45917  hoi2toco  45995  isgrim  47166  elbigofrcl  47623

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »