Theorem rneqd 5888

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

Hypothesis

Ref	Expression
rneqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
rneqd	⊢ (𝜑 → ran 𝐴 = ran 𝐵)

Proof of Theorem rneqd

Step	Hyp	Ref	Expression
1		rneqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		rneq 5886	. 2 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1542  ran crn 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-cnv 5633  df-dm 5635  df-rn 5636

This theorem is referenced by:  resima2  5976  elimampt  6003  imaeq1  6015  imaeq2  6016  mptimass  6033  resiima  6036  imadifssran  6110  rnxpid  6132  xpima  6141  funimacnv  6574  fnima  6623  focofo  6760  rnfvprc  6829  elimampo  7498  elxp4  7867  elxp5  7868  2ndval  7939  fo2nd  7957  f2ndres  7961  curry1  8048  curry2  8051  oarec  8491  en1  8965  xpassen  9003  xpdom2  9004  sbthlem4  9022  fodomr  9060  fodomfir  9232  dffi3  9338  marypha2lem4  9345  ordtypelem9  9435  dfac12lem1  10060  dfac12r  10063  fin23lem32  10260  fin23lem34  10262  fin23lem35  10263  fin23lem36  10264  fin23lem38  10265  fin23lem39  10266  fin23lem41  10268  itunitc  10337  ttukeylem3  10427  fpwwe2lem5  10552  fpwwe2lem8  10555  wunex2  10655  wuncval2  10664  gruima  10719  rpnnen1lem6  12926  hashf1lem1  14411  s1rn  14556  s2rn  14919  s3rn  14920  s7rn  14921  relexprng  15002  relexprnd  15004  relexpfld  15005  limsupval  15430  vdwapfval  16936  vdwapval  16938  vdwmc  16943  vdwpc  16945  vdwlem6  16951  vdwlem8  16953  restval  17383  restid2  17387  prdsval  17412  prdsdsval  17435  prdsdsval2  17441  prdsdsval3  17442  imasval  17469  imasdsval  17473  isfull  17873  arwval  18004  gsumvalx  18638  conjsubg  19219  psgnfval  19469  sylow1lem2  19568  sylow1lem4  19570  sylow1  19572  sylow2blem1  19589  sylow2b  19592  sylow3lem1  19596  sylow3lem2  19597  sylow3lem3  19598  sylow3lem5  19600  sylow3lem6  19601  sylow3  19602  lsmfval  19607  lsmvalx  19608  oppglsm  19611  subglsm  19642  lsmpropd  19646  efgval2  19693  efgi2  19694  efgtlen  19695  efgsdm  19699  efgsdmi  19701  efgsrel  19703  efgs1b  19705  efgsp1  19706  efgsres  19707  efgsfo  19708  efgrelexlemb  19719  frgpnabllem1  19842  iscyg  19848  iscyggen  19849  gsumxp  19945  dprdval  19974  ablfac2  20060  zncyg  21541  cygznlem2a  21560  frlmsplit2  21766  evlseu  22074  tgrest  23137  ordtval  23167  ordtbas2  23169  ordtcnv  23179  ordtrest  23180  ordtrest2  23182  ispnrm  23317  cmpfi  23386  txval  23542  xkoval  23565  ptval2  23579  ptpjopn  23590  xkoccn  23597  xkoptsub  23632  xkopt  23633  fmval  23921  fmf  23923  txflf  23984  cnextf  24044  subgntr  24085  opnsubg  24086  clsnsg  24088  snclseqg  24094  tsmsval2  24108  tsmsxplem1  24131  ustuqtoplem  24217  utopsnneiplem  24225  utopsnneip  24226  fmucndlem  24268  ressprdsds  24349  mopnval  24416  metuval  24527  metdsval  24826  lebnumlem1  24941  lebnumlem3  24943  pi1xfrcnvlem  25036  pi1xfrcnv  25037  minveclem3b  25408  elovolmr  25456  ovolctb  25470  ovoliunlem3  25484  ovolshftlem1  25489  voliunlem3  25532  voliun  25534  volsup  25536  uniioombllem2  25563  uniioombllem3  25565  mbflimsup  25646  itg1climres  25694  itg2monolem1  25730  itg2i1fseq  25735  itg2cnlem1  25741  ellimc2  25857  dvivth  25990  dvne0  25991  lhop2  25995  lhop  25996  mdegfval  26040  dchrptlem2  27245  dchrpt  27247  seqsval  28297  om2noseqfo  28307  tglnunirn  28633  tgisline  28712  perpln1  28795  perpln2  28796  isperp  28797  ishpg  28844  lmif  28870  islmib  28872  edgval  29135  edgopval  29137  edgstruct  29139  uhgr2edg  29294  usgr1e  29331  cplgrop  29523  cusgrexi  29529  structtocusgr  29532  1loopgredg  29588  1egrvtxdg0  29598  umgr2v2eedg  29611  ex-ima  30530  bafval  30693  pj3i  32297  ofrn2  32731  rnressnsn  32768  ffsrn  32819  prodindf  32940  pfxrn2  33018  pfxrn3  33019  swrdrn2  33032  swrdrn3  33033  gsumzresunsn  33141  gsumhashmul  33146  tocycfv  33188  tocycf  33196  trsp2cyc  33202  cycpmco2f1  33203  cycpmco2rn  33204  cycpmconjvlem  33220  cycpmconjslem2  33234  domnprodeq0  33355  qusbas2  33484  qusima  33486  qusrn  33487  nsgmgc  33490  nsgqusf1olem2  33492  idlsrgval  33581  esplyfval1  33735  esplyfvaln  33736  esplyind  33737  algextdeglem4  33883  smatrcl  33959  ordtprsval  34081  ordtprsuni  34082  ordtcnvNEW  34083  ordtrestNEW  34084  ordtrest2NEW  34086  qqhval  34135  qqhval2  34145  esumval  34209  esumsnf  34227  esumrnmpt2  34231  esumfsupre  34234  esumsup  34252  sxval  34353  omsval  34456  omsfval  34457  carsggect  34481  sibf0  34497  sitgfval  34504  cvmlift3lem6  35525  satfrnmapom  35571  mvtval  35701  mvrsval  35706  mrsubvrs  35723  elmsubrn  35729  msubrn  35730  mstaval  35745  msubvrs  35761  mclsval  35764  filnetlem4  36582  mptsnunlem  37671  dissneqlem  37673  exrecfnlem  37712  ctbssinf  37739  poimirlem3  37961  poimirlem9  37967  poimirlem16  37974  poimirlem17  37975  poimirlem19  37977  poimirlem20  37978  poimirlem24  37982  poimirlem30  37988  poimirlem32  37990  mblfinlem2  37996  ovoliunnfl  38000  voliunnfl  38002  isrngo  38235  drngoi  38289  rngohomval  38302  rngoisoval  38315  idlval  38351  pridlval  38371  maxidlval  38377  igenval  38399  cnvref4  38688  symrelim  38981  unidmqs  39077  lsatset  39453  docaffvalN  41584  docafvalN  41585  aks6d1c2  42586  sticksstones2  42603  sticksstones3  42604  qsalrel  42697  prjcrvfval  43081  mzpmfp  43196  eldiophb  43206  diophrw  43208  tfsconcatrn  43791  rp-tfslim  43802  conrel1d  44111  iunrelexp0  44150  rntrclfv  44180  clsneibex  44550  neicvgbex  44560  rnsnf  45635  fsneqrn  45661  limsupval3  46141  limsupresre  46145  limsupresico  46149  limsuppnfdlem  46150  limsupvaluz  46157  limsupvaluzmpt  46166  limsupvaluz2  46187  supcnvlimsup  46189  supcnvlimsupmpt  46190  liminfval  46208  liminfval5  46214  limsupresxr  46215  liminfresxr  46216  liminfresico  46220  liminfvalxr  46232  fourierdlem60  46615  fourierdlem61  46616  sge0val  46815  sge0z  46824  sge0revalmpt  46827  sge0tsms  46829  sge0sup  46840  sge0split  46858  sge0fodjrnlem  46865  sge0seq  46895  meadjiunlem  46914  meaiuninclem  46929  omeiunle  46966  ovolval2lem  47092  ovolval4lem2  47099  ovolval5lem2  47102  ovolval5lem3  47103  ovolval5  47104  ovnovollem2  47106  smfsuplem2  47261  smfsup  47263  smfsupmpt  47264  smfinf  47267  smfinfmpt  47268  smflimsuplem1  47269  smflimsuplem2  47270  smflimsuplem4  47272  smflimsuplem5  47273  smflimsuplem7  47275  smflimsup  47277  fnrnafv  47625  afv2eq12d  47678  isubgredgss  48356  isubgredg  48357  stgredg  48447  gpgedg  48536  dmrnxp  49327  imaidfu  49600  idfudiag1lem  50013