Theorem rneqd 5928

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

Syntax hints:   → wi 4   = wceq 1570  ran crn 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-cnv 5669  df-dm 5671  df-rn 5672

This theorem is referenced by:  resima2  6015  elimampt  6045  imaeq1  6057  imaeq2  6058  mptimass  6075  resiima  6078  rnxpid  6171  xpima  6180  imadifssranOLD  6203  funimacnv  6617  fnima  6665  focofo  6805  rnfvprc  6875  elimampo  7547  elxp4  7915  elxp5  7916  2ndval  7985  fo2nd  8003  f2ndres  8007  curry1  8095  curry2  8098  oarec  8543  en1  9017  xpassen  9055  xpdom2  9056  sbthlem4  9074  fodomr  9112  fodomfir  9283  dffi3  9387  marypha2lem4  9394  ordtypelem9  9484  dfac12lem1  10123  dfac12r  10126  fin23lem32  10323  fin23lem34  10325  fin23lem35  10326  fin23lem36  10327  fin23lem38  10328  fin23lem39  10329  fin23lem41  10331  itunitc  10400  ttukeylem3  10490  fpwwe2lem5  10615  fpwwe2lem8  10618  wunex2  10718  wuncval2  10727  gruima  10782  rpnnen1lem6  13001  hashf1lem1  14488  s1rn  14633  s2rn  14996  s3rn  14997  s7rn  14998  relexprng  15079  relexprnd  15081  relexpfld  15082  limsupval  15521  vdwapfval  17026  vdwapval  17028  vdwmc  17033  vdwpc  17035  vdwlem6  17041  vdwlem8  17043  restval  17474  restid2  17478  prdsval  17503  prdsdsval  17526  prdsdsval2  17532  prdsdsval3  17533  imasval  17560  imasdsval  17564  isfull  17964  arwval  18095  gsumvalx  18729  conjsubg  19315  psgnfval  19565  sylow1lem2  19664  sylow1lem4  19666  sylow1  19668  sylow2blem1  19685  sylow2b  19688  sylow3lem1  19692  sylow3lem2  19693  sylow3lem3  19694  sylow3lem5  19696  sylow3lem6  19697  sylow3  19698  lsmfval  19703  lsmvalx  19704  oppglsm  19707  subglsm  19738  lsmpropd  19742  efgval2  19789  efgi2  19790  efgtlen  19791  efgsdm  19795  efgsdmi  19797  efgsrel  19799  efgs1b  19801  efgsp1  19802  efgsres  19803  efgsfo  19804  efgrelexlemb  19815  frgpnabllem1  19938  iscyg  19944  iscyggen  19945  gsumxp  20041  dprdval  20070  ablfac2  20156  zncyg  21698  cygznlem2a  21717  frlmsplit2  21923  evlseu  22234  tgrest  23316  ordtval  23346  ordtbas2  23348  ordtcnv  23358  ordtrest  23359  ordtrest2  23361  ispnrm  23496  cmpfi  23565  txval  23721  xkoval  23744  ptval2  23758  ptpjopn  23769  xkoccn  23776  xkoptsub  23811  xkopt  23812  fmval  24100  fmf  24102  txflf  24163  cnextf  24223  subgntr  24264  opnsubg  24265  clsnsg  24267  snclseqg  24273  tsmsval2  24287  tsmsxplem1  24310  ustuqtoplem  24396  utopsnneiplem  24404  utopsnneip  24405  fmucndlem  24447  ressprdsds  24528  mopnval  24595  metuval  24706  metdsval  25005  lebnumlem1  25120  lebnumlem3  25122  pi1xfrcnvlem  25215  pi1xfrcnv  25216  minveclem3b  25587  elovolmr  25635  ovolctb  25649  ovoliunlem3  25663  ovolshftlem1  25668  voliunlem3  25711  voliun  25713  volsup  25715  uniioombllem2  25742  uniioombllem3  25744  mbflimsup  25825  itg1climres  25873  itg2monolem1  25909  itg2i1fseq  25914  itg2cnlem1  25920  ellimc2  26036  dvivth  26169  dvne0  26170  lhop2  26174  lhop  26175  mdegfval  26219  dchrptlem2  27429  dchrpt  27431  seqsval  28481  om2noseqfo  28491  tglnunirn  28817  tgisline  28900  perpln1  28990  perpln2  28991  isperp  28992  ishpg  29041  tgplnfn  29057  plngval  29059  isplng  29060  lmif  29094  islmib  29096  brprlng  29188  edgval  29399  edgopval  29401  edgstruct  29403  uhgr2edg  29558  usgr1e  29595  cplgrop  29787  cusgrexi  29793  structtocusgr  29796  1loopgredg  29851  1egrvtxdg0  29861  umgr2v2eedg  29874  ex-ima  30793  bafval  30956  pj3i  32560  ofrn2  32985  rnressnsn  33022  ffsrn  33073  prodindf  33182  pfxrn2  33260  pfxrn3  33261  swrdrn2  33274  swrdrn3  33275  gsumzresunsn  33382  gsumhashmul  33387  tocycfv  33429  tocycf  33437  trsp2cyc  33443  cycpmco2f1  33444  cycpmco2rn  33445  cycpmconjvlem  33461  cycpmconjslem2  33475  domnprodeq0  33599  qusbas2  33715  qusima  33717  qusrn  33718  nsgmgc  33721  nsgqusf1olem2  33723  idlsrgval  33793  esplyfval1  33963  esplyfvaln  33964  esplyind  33965  algextdeglem4  34110  smatrcl  34186  ordtprsval  34308  ordtprsuni  34309  ordtcnvNEW  34310  ordtrestNEW  34311  ordtrest2NEW  34313  qqhval  34362  qqhval2  34372  esumval  34436  esumsnf  34454  esumrnmpt2  34458  esumfsupre  34461  esumsup  34479  sxval  34580  omsval  34683  omsfval  34684  carsggect  34708  sibf0  34724  sitgfval  34731  cvmlift3lem6  35816  satfrnmapom  35862  mvtval  35992  mvrsval  35997  mrsubvrs  36014  elmsubrn  36020  msubrn  36021  mstaval  36036  msubvrs  36052  mclsval  36055  filnetlem4  36892  mptsnunlem  37984  dissneqlem  37986  exrecfnlem  38025  ctbssinf  38052  poimirlem3  38274  poimirlem9  38280  poimirlem16  38287  poimirlem17  38288  poimirlem19  38290  poimirlem20  38291  poimirlem24  38295  poimirlem30  38301  poimirlem32  38303  mblfinlem2  38309  ovoliunnfl  38313  voliunnfl  38315  isrngo  38548  drngoi  38602  rngohomval  38615  rngoisoval  38628  idlval  38664  pridlval  38684  maxidlval  38690  igenval  38712  cnvref4  38999  symrelim  39292  unidmqs  39388  lsatset  39764  docaffvalN  41895  docafvalN  41896  aks6d1c2  42897  sticksstones2  42914  sticksstones3  42915  qsalrel  43009  prjcrvfval  43363  mzpmfp  43478  eldiophb  43488  diophrw  43490  tfsconcatrn  44069  rp-tfslim  44080  conrel1d  44389  iunrelexp0  44428  rntrclfv  44458  clsneibex  44828  neicvgbex  44838  rnsnf  45902  fsneqrn  45927  limsupval3  46406  limsupresre  46410  limsupresico  46414  limsuppnfdlem  46415  limsupvaluz  46422  limsupvaluzmpt  46431  limsupvaluz2  46452  supcnvlimsup  46454  supcnvlimsupmpt  46455  liminfval  46473  liminfval5  46479  limsupresxr  46480  liminfresxr  46481  liminfresico  46485  liminfvalxr  46497  fourierdlem60  46880  fourierdlem61  46881  sge0val  47080  sge0z  47089  sge0revalmpt  47092  sge0tsms  47094  sge0sup  47105  sge0split  47123  sge0fodjrnlem  47130  sge0seq  47160  meadjiunlem  47179  meaiuninclem  47194  omeiunle  47231  ovolval2lem  47357  ovolval4lem2  47364  ovolval5lem2  47367  ovolval5lem3  47368  ovolval5  47369  ovnovollem2  47371  smfsuplem2  47526  smfsup  47528  smfsupmpt  47529  smfinf  47532  smfinfmpt  47533  smflimsuplem1  47534  smflimsuplem2  47535  smflimsuplem4  47537  smflimsuplem5  47538  smflimsuplem7  47540  smflimsup  47542  fnrnafv  47899  afv2eq12d  47952  isubgredgss  48630  isubgredg  48631  stgredg  48721  gpgedg  48810  dmrnxp  49615  imaidfu  49888  idfudiag1lem  50301