Theorem rneqd 5902

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

Syntax hints:   → wi 4   = wceq 1540  ran crn 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-cnv 5646  df-dm 5648  df-rn 5649

This theorem is referenced by:  resima2  5987  elimampt  6014  imaeq1  6026  imaeq2  6027  mptimass  6044  resiima  6047  imadifssran  6124  rnxpid  6146  xpima  6155  funimacnv  6597  fnima  6648  focofo  6785  rnfvprc  6852  elimampo  7526  elxp4  7898  elxp5  7899  2ndval  7971  fo2nd  7989  f2ndres  7993  curry1  8083  curry2  8086  oarec  8526  en1  8995  xpassen  9035  xpdom2  9036  sbthlem4  9054  fodomr  9092  fodomfir  9279  dffi3  9382  marypha2lem4  9389  ordtypelem9  9479  dfac12lem1  10097  dfac12r  10100  fin23lem32  10297  fin23lem34  10299  fin23lem35  10300  fin23lem36  10301  fin23lem38  10302  fin23lem39  10303  fin23lem41  10305  itunitc  10374  ttukeylem3  10464  fpwwe2lem5  10588  fpwwe2lem8  10591  wunex2  10691  wuncval2  10700  gruima  10755  rpnnen1lem6  12941  hashf1lem1  14420  s1rn  14564  s2rn  14929  s3rn  14930  s7rn  14931  relexprng  15012  relexprnd  15014  relexpfld  15015  limsupval  15440  vdwapfval  16942  vdwapval  16944  vdwmc  16949  vdwpc  16951  vdwlem6  16957  vdwlem8  16959  restval  17389  restid2  17393  prdsval  17418  prdsdsval  17441  prdsdsval2  17447  prdsdsval3  17448  imasval  17474  imasdsval  17478  isfull  17874  arwval  18005  gsumvalx  18603  conjsubg  19182  psgnfval  19430  sylow1lem2  19529  sylow1lem4  19531  sylow1  19533  sylow2blem1  19550  sylow2b  19553  sylow3lem1  19557  sylow3lem2  19558  sylow3lem3  19559  sylow3lem5  19561  sylow3lem6  19562  sylow3  19563  lsmfval  19568  lsmvalx  19569  oppglsm  19572  subglsm  19603  lsmpropd  19607  efgval2  19654  efgi2  19655  efgtlen  19656  efgsdm  19660  efgsdmi  19662  efgsrel  19664  efgs1b  19666  efgsp1  19667  efgsres  19668  efgsfo  19669  efgrelexlemb  19680  frgpnabllem1  19803  iscyg  19809  iscyggen  19810  gsumxp  19906  dprdval  19935  ablfac2  20021  zncyg  21458  cygznlem2a  21477  frlmsplit2  21682  evlseu  21990  tgrest  23046  ordtval  23076  ordtbas2  23078  ordtcnv  23088  ordtrest  23089  ordtrest2  23091  ispnrm  23226  cmpfi  23295  txval  23451  xkoval  23474  ptval2  23488  ptpjopn  23499  xkoccn  23506  xkoptsub  23541  xkopt  23542  fmval  23830  fmf  23832  txflf  23893  cnextf  23953  subgntr  23994  opnsubg  23995  clsnsg  23997  snclseqg  24003  tsmsval2  24017  tsmsxplem1  24040  ustuqtoplem  24127  utopsnneiplem  24135  utopsnneip  24136  fmucndlem  24178  ressprdsds  24259  mopnval  24326  metuval  24437  metdsval  24736  lebnumlem1  24860  lebnumlem3  24862  pi1xfrcnvlem  24956  pi1xfrcnv  24957  minveclem3b  25328  elovolmr  25377  ovolctb  25391  ovoliunlem3  25405  ovolshftlem1  25410  voliunlem3  25453  voliun  25455  volsup  25457  uniioombllem2  25484  uniioombllem3  25486  mbflimsup  25567  itg1climres  25615  itg2monolem1  25651  itg2i1fseq  25656  itg2cnlem1  25662  ellimc2  25778  dvivth  25915  dvne0  25916  lhop2  25920  lhop  25921  mdegfval  25967  dchrptlem2  27176  dchrpt  27178  seqsval  28182  om2noseqfo  28192  tglnunirn  28475  tgisline  28554  perpln1  28637  perpln2  28638  isperp  28639  ishpg  28686  lmif  28712  islmib  28714  edgval  28976  edgopval  28978  edgstruct  28980  uhgr2edg  29135  usgr1e  29172  cplgrop  29364  cusgrexi  29370  structtocusgr  29373  1loopgredg  29429  1egrvtxdg0  29439  umgr2v2eedg  29452  ex-ima  30371  bafval  30533  pj3i  32137  ofrn2  32564  ffsrn  32652  prodindf  32786  pfxrn2  32861  pfxrn3  32862  swrdrn2  32876  swrdrn3  32877  gsumzresunsn  32996  gsumhashmul  33001  tocycfv  33066  tocycf  33074  trsp2cyc  33080  cycpmco2f1  33081  cycpmco2rn  33082  cycpmconjvlem  33098  cycpmconjslem2  33112  qusbas2  33377  qusima  33379  qusrn  33380  nsgmgc  33383  nsgqusf1olem2  33385  idlsrgval  33474  algextdeglem4  33710  smatrcl  33786  ordtprsval  33908  ordtprsuni  33909  ordtcnvNEW  33910  ordtrestNEW  33911  ordtrest2NEW  33913  qqhval  33962  qqhval2  33972  esumval  34036  esumsnf  34054  esumrnmpt2  34058  esumfsupre  34061  esumsup  34079  sxval  34180  omsval  34284  omsfval  34285  carsggect  34309  sibf0  34325  sitgfval  34332  cvmlift3lem6  35311  satfrnmapom  35357  mvtval  35487  mvrsval  35492  mrsubvrs  35509  elmsubrn  35515  msubrn  35516  mstaval  35531  msubvrs  35547  mclsval  35550  filnetlem4  36369  mptsnunlem  37326  dissneqlem  37328  exrecfnlem  37367  ctbssinf  37394  poimirlem3  37617  poimirlem9  37623  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem24  37638  poimirlem30  37644  poimirlem32  37646  mblfinlem2  37652  ovoliunnfl  37656  voliunnfl  37658  isrngo  37891  drngoi  37945  rngohomval  37958  rngoisoval  37971  idlval  38007  pridlval  38027  maxidlval  38033  igenval  38055  cnvref4  38332  symrelim  38550  unidmqs  38646  lsatset  38983  docaffvalN  41115  docafvalN  41116  aks6d1c2  42118  sticksstones2  42135  sticksstones3  42136  qsalrel  42228  prjcrvfval  42619  mzpmfp  42735  eldiophb  42745  diophrw  42747  tfsconcatrn  43331  rp-tfslim  43342  conrel1d  43652  iunrelexp0  43691  rntrclfv  43721  clsneibex  44091  neicvgbex  44101  rnsnf  45178  fsneqrn  45205  limsupval3  45690  limsupresre  45694  limsupresico  45698  limsuppnfdlem  45699  limsupvaluz  45706  limsupvaluzmpt  45715  limsupvaluz2  45736  supcnvlimsup  45738  supcnvlimsupmpt  45739  liminfval  45757  liminfval5  45763  limsupresxr  45764  liminfresxr  45765  liminfresico  45769  liminfvalxr  45781  fourierdlem60  46164  fourierdlem61  46165  sge0val  46364  sge0z  46373  sge0revalmpt  46376  sge0tsms  46378  sge0sup  46389  sge0split  46407  sge0fodjrnlem  46414  sge0seq  46444  meadjiunlem  46463  meaiuninclem  46478  omeiunle  46515  ovolval2lem  46641  ovolval4lem2  46648  ovolval5lem2  46651  ovolval5lem3  46652  ovolval5  46653  ovnovollem2  46655  smfsuplem2  46810  smfsup  46812  smfsupmpt  46813  smfinf  46816  smfinfmpt  46817  smflimsuplem1  46818  smflimsuplem2  46819  smflimsuplem4  46821  smflimsuplem5  46822  smflimsuplem7  46824  smflimsup  46826  fnrnafv  47163  afv2eq12d  47216  isubgredgss  47865  isubgredg  47866  stgredg  47955  gpgedg  48036  dmrnxp  48825  imaidfu  49099  idfudiag1lem  49512