Theorem rneqd 5792

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 5790	. 2 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1543  ran crn 5537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-br 5040  df-opab 5102  df-cnv 5544  df-dm 5546  df-rn 5547

This theorem is referenced by:  resima2  5871  imaeq1  5909  imaeq2  5910  resiima  5929  rnxpid  6016  xpima  6025  funimacnv  6439  fnima  6486  focofo  6624  rnfvprc  6689  elxp4  7678  elxp5  7679  2ndval  7742  fo2nd  7760  f2ndres  7764  curry1  7850  curry2  7853  oarec  8268  en1  8676  en1OLD  8677  xpassen  8717  xpdom2  8718  sbthlem4  8737  fodomr  8775  dffi3  9025  marypha2lem4  9032  ordtypelem9  9120  trpredeq1  9303  trpredeq2  9304  trpredeq3  9305  dfac12lem1  9722  dfac12r  9725  fin23lem32  9923  fin23lem34  9925  fin23lem35  9926  fin23lem36  9927  fin23lem38  9928  fin23lem39  9929  fin23lem41  9931  itunitc  10000  ttukeylem3  10090  fpwwe2lem5  10214  fpwwe2lem8  10217  wunex2  10317  wuncval2  10326  gruima  10381  rpnnen1lem6  12543  hashf1lem1  13985  hashf1lem1OLD  13986  s1rn  14121  relexprng  14574  relexprnd  14576  relexpfld  14577  limsupval  15000  vdwapfval  16487  vdwapval  16489  vdwmc  16494  vdwpc  16496  vdwlem6  16502  vdwlem8  16504  restval  16885  restid2  16889  prdsval  16914  prdsdsval  16937  prdsdsval2  16943  prdsdsval3  16944  imasval  16970  imasdsval  16974  isfull  17371  arwval  17503  gsumvalx  18102  conjsubg  18608  psgnfval  18846  sylow1lem2  18942  sylow1lem4  18944  sylow1  18946  sylow2blem1  18963  sylow2b  18966  sylow3lem1  18970  sylow3lem2  18971  sylow3lem3  18972  sylow3lem5  18974  sylow3lem6  18975  sylow3  18976  lsmfval  18981  lsmvalx  18982  oppglsm  18985  subglsm  19017  lsmpropd  19021  efgval2  19068  efgi2  19069  efgtlen  19070  efgsdm  19074  efgsdmi  19076  efgsrel  19078  efgs1b  19080  efgsp1  19081  efgsres  19082  efgsfo  19083  efgrelexlemb  19094  frgpnabllem1  19212  iscyg  19217  iscyggen  19218  gsumxp  19315  dprdval  19344  ablfac2  19430  rnrhmsubrg  19786  zncyg  20467  cygznlem2a  20486  frlmsplit2  20689  evlseu  20997  tgrest  22010  ordtval  22040  ordtbas2  22042  ordtcnv  22052  ordtrest  22053  ordtrest2  22055  ispnrm  22190  cmpfi  22259  txval  22415  xkoval  22438  ptval2  22452  ptpjopn  22463  xkoccn  22470  xkoptsub  22505  xkopt  22506  fmval  22794  fmf  22796  txflf  22857  cnextf  22917  subgntr  22958  opnsubg  22959  clsnsg  22961  snclseqg  22967  tsmsval2  22981  tsmsxplem1  23004  ustuqtoplem  23091  utopsnneiplem  23099  utopsnneip  23100  fmucndlem  23142  ressprdsds  23223  mopnval  23290  metuval  23401  metdsval  23698  lebnumlem1  23812  lebnumlem3  23814  pi1xfrcnvlem  23907  pi1xfrcnv  23908  minveclem3b  24279  elovolmr  24327  ovolctb  24341  ovoliunlem3  24355  ovolshftlem1  24360  voliunlem3  24403  voliun  24405  volsup  24407  uniioombllem2  24434  uniioombllem3  24436  mbflimsup  24517  itg1climres  24566  itg2monolem1  24602  itg2i1fseq  24607  itg2cnlem1  24613  ellimc2  24728  dvivth  24861  dvne0  24862  lhop2  24866  lhop  24867  mdegfval  24914  dchrptlem2  26100  dchrpt  26102  tglnunirn  26593  tgisline  26672  perpln1  26755  perpln2  26756  isperp  26757  ishpg  26804  lmif  26830  islmib  26832  edgval  27094  edgopval  27096  edgstruct  27098  uhgr2edg  27250  usgr1e  27287  cplgrop  27479  cusgrexi  27485  structtocusgr  27488  1loopgredg  27543  1egrvtxdg0  27553  umgr2v2eedg  27566  ex-ima  28479  bafval  28639  pj3i  30243  elimampt  30646  ofrn2  30650  ffsrn  30738  pfxrn2  30888  pfxrn3  30889  swrdrn2  30900  swrdrn3  30901  gsumzresunsn  30987  gsumhashmul  30989  tocycfv  31049  tocycf  31057  trsp2cyc  31063  cycpmco2f1  31064  cycpmco2rn  31065  cycpmconjvlem  31081  cycpmconjslem2  31095  qusima  31262  nsgmgc  31265  nsgqusf1olem2  31267  idlsrgval  31316  smatrcl  31414  ordtprsval  31536  ordtprsuni  31537  ordtcnvNEW  31538  ordtrestNEW  31539  ordtrest2NEW  31541  qqhval  31590  qqhval2  31598  prodindf  31657  esumval  31680  esumsnf  31698  esumrnmpt2  31702  esumfsupre  31705  esumsup  31723  sxval  31824  omsval  31926  omsfval  31927  carsggect  31951  sibf0  31967  sitgfval  31974  cvmlift3lem6  32953  satfrnmapom  32999  mvtval  33129  mvrsval  33134  mrsubvrs  33151  elmsubrn  33157  msubrn  33158  mstaval  33173  msubvrs  33189  mclsval  33192  filnetlem4  34256  mptsnunlem  35195  dissneqlem  35197  exrecfnlem  35236  ctbssinf  35263  poimirlem3  35466  poimirlem9  35472  poimirlem16  35479  poimirlem17  35480  poimirlem19  35482  poimirlem20  35483  poimirlem24  35487  poimirlem30  35493  poimirlem32  35495  mblfinlem2  35501  ovoliunnfl  35505  voliunnfl  35507  isrngo  35741  drngoi  35795  rngohomval  35808  rngoisoval  35821  idlval  35857  pridlval  35877  maxidlval  35883  igenval  35905  symrelim  36359  unidmqs  36452  lsatset  36690  docaffvalN  38821  docafvalN  38822  sticksstones2  39772  sticksstones3  39773  qsalrel  39869  mzpmfp  40213  eldiophb  40223  diophrw  40225  conrel1d  40889  iunrelexp0  40928  rntrclfv  40958  clsneibex  41330  neicvgbex  41340  rnsnf  42335  fsneqrn  42365  mptima2  42404  limsupval3  42851  limsupresre  42855  limsupresico  42859  limsuppnfdlem  42860  limsupvaluz  42867  limsupvaluzmpt  42876  limsupvaluz2  42897  supcnvlimsup  42899  supcnvlimsupmpt  42900  liminfval  42918  liminfval5  42924  limsupresxr  42925  liminfresxr  42926  liminfresico  42930  liminfvalxr  42942  fourierdlem60  43325  fourierdlem61  43326  sge0val  43522  sge0z  43531  sge0revalmpt  43534  sge0tsms  43536  sge0sup  43547  sge0split  43565  sge0fodjrnlem  43572  sge0seq  43602  meadjiunlem  43621  meaiuninclem  43636  omeiunle  43673  ovolval2lem  43799  ovolval4lem2  43806  ovolval5lem2  43809  ovolval5lem3  43810  ovolval5  43811  ovnovollem2  43813  smfsuplem2  43960  smfsup  43962  smfsupmpt  43963  smfinf  43966  smfinfmpt  43967  smflimsuplem1  43968  smflimsuplem2  43969  smflimsuplem4  43971  smflimsuplem5  43972  smflimsuplem7  43974  smflimsup  43976  fnrnafv  44269  afv2eq12d  44322