Theorem rneqd 5885

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

Syntax hints:   → wi 4   = wceq 1541  ran crn 5623

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-cnv 5630  df-dm 5632  df-rn 5633

This theorem is referenced by:  resima2  5973  elimampt  6000  imaeq1  6012  imaeq2  6013  mptimass  6030  resiima  6033  imadifssran  6107  rnxpid  6129  xpima  6138  funimacnv  6571  fnima  6620  focofo  6757  rnfvprc  6826  elimampo  7493  elxp4  7862  elxp5  7863  2ndval  7934  fo2nd  7952  f2ndres  7956  curry1  8044  curry2  8047  oarec  8487  en1  8959  xpassen  8997  xpdom2  8998  sbthlem4  9016  fodomr  9054  fodomfir  9226  dffi3  9332  marypha2lem4  9339  ordtypelem9  9429  dfac12lem1  10052  dfac12r  10055  fin23lem32  10252  fin23lem34  10254  fin23lem35  10255  fin23lem36  10256  fin23lem38  10257  fin23lem39  10258  fin23lem41  10260  itunitc  10329  ttukeylem3  10419  fpwwe2lem5  10544  fpwwe2lem8  10547  wunex2  10647  wuncval2  10656  gruima  10711  rpnnen1lem6  12893  hashf1lem1  14376  s1rn  14521  s2rn  14884  s3rn  14885  s7rn  14886  relexprng  14967  relexprnd  14969  relexpfld  14970  limsupval  15395  vdwapfval  16897  vdwapval  16899  vdwmc  16904  vdwpc  16906  vdwlem6  16912  vdwlem8  16914  restval  17344  restid2  17348  prdsval  17373  prdsdsval  17396  prdsdsval2  17402  prdsdsval3  17403  imasval  17430  imasdsval  17434  isfull  17834  arwval  17965  gsumvalx  18599  conjsubg  19177  psgnfval  19427  sylow1lem2  19526  sylow1lem4  19528  sylow1  19530  sylow2blem1  19547  sylow2b  19550  sylow3lem1  19554  sylow3lem2  19555  sylow3lem3  19556  sylow3lem5  19558  sylow3lem6  19559  sylow3  19560  lsmfval  19565  lsmvalx  19566  oppglsm  19569  subglsm  19600  lsmpropd  19604  efgval2  19651  efgi2  19652  efgtlen  19653  efgsdm  19657  efgsdmi  19659  efgsrel  19661  efgs1b  19663  efgsp1  19664  efgsres  19665  efgsfo  19666  efgrelexlemb  19677  frgpnabllem1  19800  iscyg  19806  iscyggen  19807  gsumxp  19903  dprdval  19932  ablfac2  20018  zncyg  21501  cygznlem2a  21520  frlmsplit2  21726  evlseu  22036  tgrest  23101  ordtval  23131  ordtbas2  23133  ordtcnv  23143  ordtrest  23144  ordtrest2  23146  ispnrm  23281  cmpfi  23350  txval  23506  xkoval  23529  ptval2  23543  ptpjopn  23554  xkoccn  23561  xkoptsub  23596  xkopt  23597  fmval  23885  fmf  23887  txflf  23948  cnextf  24008  subgntr  24049  opnsubg  24050  clsnsg  24052  snclseqg  24058  tsmsval2  24072  tsmsxplem1  24095  ustuqtoplem  24181  utopsnneiplem  24189  utopsnneip  24190  fmucndlem  24232  ressprdsds  24313  mopnval  24380  metuval  24491  metdsval  24790  lebnumlem1  24914  lebnumlem3  24916  pi1xfrcnvlem  25010  pi1xfrcnv  25011  minveclem3b  25382  elovolmr  25431  ovolctb  25445  ovoliunlem3  25459  ovolshftlem1  25464  voliunlem3  25507  voliun  25509  volsup  25511  uniioombllem2  25538  uniioombllem3  25540  mbflimsup  25621  itg1climres  25669  itg2monolem1  25705  itg2i1fseq  25710  itg2cnlem1  25716  ellimc2  25832  dvivth  25969  dvne0  25970  lhop2  25974  lhop  25975  mdegfval  26021  dchrptlem2  27230  dchrpt  27232  seqsval  28249  om2noseqfo  28259  tglnunirn  28569  tgisline  28648  perpln1  28731  perpln2  28732  isperp  28733  ishpg  28780  lmif  28806  islmib  28808  edgval  29071  edgopval  29073  edgstruct  29075  uhgr2edg  29230  usgr1e  29267  cplgrop  29459  cusgrexi  29465  structtocusgr  29468  1loopgredg  29524  1egrvtxdg0  29534  umgr2v2eedg  29547  ex-ima  30466  bafval  30628  pj3i  32232  ofrn2  32667  rnressnsn  32705  ffsrn  32756  prodindf  32893  pfxrn2  32971  pfxrn3  32972  swrdrn2  32985  swrdrn3  32986  gsumzresunsn  33094  gsumhashmul  33099  tocycfv  33140  tocycf  33148  trsp2cyc  33154  cycpmco2f1  33155  cycpmco2rn  33156  cycpmconjvlem  33172  cycpmconjslem2  33186  domnprodeq0  33307  qusbas2  33436  qusima  33438  qusrn  33439  nsgmgc  33442  nsgqusf1olem2  33444  idlsrgval  33533  esplyind  33680  algextdeglem4  33826  smatrcl  33902  ordtprsval  34024  ordtprsuni  34025  ordtcnvNEW  34026  ordtrestNEW  34027  ordtrest2NEW  34029  qqhval  34078  qqhval2  34088  esumval  34152  esumsnf  34170  esumrnmpt2  34174  esumfsupre  34177  esumsup  34195  sxval  34296  omsval  34399  omsfval  34400  carsggect  34424  sibf0  34440  sitgfval  34447  cvmlift3lem6  35467  satfrnmapom  35513  mvtval  35643  mvrsval  35648  mrsubvrs  35665  elmsubrn  35671  msubrn  35672  mstaval  35687  msubvrs  35703  mclsval  35706  filnetlem4  36524  mptsnunlem  37482  dissneqlem  37484  exrecfnlem  37523  ctbssinf  37550  poimirlem3  37763  poimirlem9  37769  poimirlem16  37776  poimirlem17  37777  poimirlem19  37779  poimirlem20  37780  poimirlem24  37784  poimirlem30  37790  poimirlem32  37792  mblfinlem2  37798  ovoliunnfl  37802  voliunnfl  37804  isrngo  38037  drngoi  38091  rngohomval  38104  rngoisoval  38117  idlval  38153  pridlval  38173  maxidlval  38179  igenval  38201  cnvref4  38482  symrelim  38755  unidmqs  38852  lsatset  39189  docaffvalN  41320  docafvalN  41321  aks6d1c2  42323  sticksstones2  42340  sticksstones3  42341  qsalrel  42438  prjcrvfval  42816  mzpmfp  42931  eldiophb  42941  diophrw  42943  tfsconcatrn  43526  rp-tfslim  43537  conrel1d  43846  iunrelexp0  43885  rntrclfv  43915  clsneibex  44285  neicvgbex  44295  rnsnf  45370  fsneqrn  45397  limsupval3  45878  limsupresre  45882  limsupresico  45886  limsuppnfdlem  45887  limsupvaluz  45894  limsupvaluzmpt  45903  limsupvaluz2  45924  supcnvlimsup  45926  supcnvlimsupmpt  45927  liminfval  45945  liminfval5  45951  limsupresxr  45952  liminfresxr  45953  liminfresico  45957  liminfvalxr  45969  fourierdlem60  46352  fourierdlem61  46353  sge0val  46552  sge0z  46561  sge0revalmpt  46564  sge0tsms  46566  sge0sup  46577  sge0split  46595  sge0fodjrnlem  46602  sge0seq  46632  meadjiunlem  46651  meaiuninclem  46666  omeiunle  46703  ovolval2lem  46829  ovolval4lem2  46836  ovolval5lem2  46839  ovolval5lem3  46840  ovolval5  46841  ovnovollem2  46843  smfsuplem2  46998  smfsup  47000  smfsupmpt  47001  smfinf  47004  smfinfmpt  47005  smflimsuplem1  47006  smflimsuplem2  47007  smflimsuplem4  47009  smflimsuplem5  47010  smflimsuplem7  47012  smflimsup  47014  fnrnafv  47350  afv2eq12d  47403  isubgredgss  48053  isubgredg  48054  stgredg  48144  gpgedg  48233  dmrnxp  49024  imaidfu  49297  idfudiag1lem  49710