Theorem rneqd 5880

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

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

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-cnv 5627  df-dm 5629  df-rn 5630

This theorem is referenced by:  resima2  5967  elimampt  5994  imaeq1  6006  imaeq2  6007  mptimass  6024  resiima  6027  imadifssran  6100  rnxpid  6122  xpima  6131  funimacnv  6563  fnima  6612  focofo  6749  rnfvprc  6816  elimampo  7486  elxp4  7855  elxp5  7856  2ndval  7927  fo2nd  7945  f2ndres  7949  curry1  8037  curry2  8040  oarec  8480  en1  8949  xpassen  8988  xpdom2  8989  sbthlem4  9007  fodomr  9045  fodomfir  9218  dffi3  9321  marypha2lem4  9328  ordtypelem9  9418  dfac12lem1  10038  dfac12r  10041  fin23lem32  10238  fin23lem34  10240  fin23lem35  10241  fin23lem36  10242  fin23lem38  10243  fin23lem39  10244  fin23lem41  10246  itunitc  10315  ttukeylem3  10405  fpwwe2lem5  10529  fpwwe2lem8  10532  wunex2  10632  wuncval2  10641  gruima  10696  rpnnen1lem6  12883  hashf1lem1  14362  s1rn  14506  s2rn  14870  s3rn  14871  s7rn  14872  relexprng  14953  relexprnd  14955  relexpfld  14956  limsupval  15381  vdwapfval  16883  vdwapval  16885  vdwmc  16890  vdwpc  16892  vdwlem6  16898  vdwlem8  16900  restval  17330  restid2  17334  prdsval  17359  prdsdsval  17382  prdsdsval2  17388  prdsdsval3  17389  imasval  17415  imasdsval  17419  isfull  17819  arwval  17950  gsumvalx  18550  conjsubg  19129  psgnfval  19379  sylow1lem2  19478  sylow1lem4  19480  sylow1  19482  sylow2blem1  19499  sylow2b  19502  sylow3lem1  19506  sylow3lem2  19507  sylow3lem3  19508  sylow3lem5  19510  sylow3lem6  19511  sylow3  19512  lsmfval  19517  lsmvalx  19518  oppglsm  19521  subglsm  19552  lsmpropd  19556  efgval2  19603  efgi2  19604  efgtlen  19605  efgsdm  19609  efgsdmi  19611  efgsrel  19613  efgs1b  19615  efgsp1  19616  efgsres  19617  efgsfo  19618  efgrelexlemb  19629  frgpnabllem1  19752  iscyg  19758  iscyggen  19759  gsumxp  19855  dprdval  19884  ablfac2  19970  zncyg  21455  cygznlem2a  21474  frlmsplit2  21680  evlseu  21988  tgrest  23044  ordtval  23074  ordtbas2  23076  ordtcnv  23086  ordtrest  23087  ordtrest2  23089  ispnrm  23224  cmpfi  23293  txval  23449  xkoval  23472  ptval2  23486  ptpjopn  23497  xkoccn  23504  xkoptsub  23539  xkopt  23540  fmval  23828  fmf  23830  txflf  23891  cnextf  23951  subgntr  23992  opnsubg  23993  clsnsg  23995  snclseqg  24001  tsmsval2  24015  tsmsxplem1  24038  ustuqtoplem  24125  utopsnneiplem  24133  utopsnneip  24134  fmucndlem  24176  ressprdsds  24257  mopnval  24324  metuval  24435  metdsval  24734  lebnumlem1  24858  lebnumlem3  24860  pi1xfrcnvlem  24954  pi1xfrcnv  24955  minveclem3b  25326  elovolmr  25375  ovolctb  25389  ovoliunlem3  25403  ovolshftlem1  25408  voliunlem3  25451  voliun  25453  volsup  25455  uniioombllem2  25482  uniioombllem3  25484  mbflimsup  25565  itg1climres  25613  itg2monolem1  25649  itg2i1fseq  25654  itg2cnlem1  25660  ellimc2  25776  dvivth  25913  dvne0  25914  lhop2  25918  lhop  25919  mdegfval  25965  dchrptlem2  27174  dchrpt  27176  seqsval  28187  om2noseqfo  28197  tglnunirn  28493  tgisline  28572  perpln1  28655  perpln2  28656  isperp  28657  ishpg  28704  lmif  28730  islmib  28732  edgval  28994  edgopval  28996  edgstruct  28998  uhgr2edg  29153  usgr1e  29190  cplgrop  29382  cusgrexi  29388  structtocusgr  29391  1loopgredg  29447  1egrvtxdg0  29457  umgr2v2eedg  29470  ex-ima  30386  bafval  30548  pj3i  32152  ofrn2  32583  ffsrn  32672  prodindf  32806  pfxrn2  32881  pfxrn3  32882  swrdrn2  32896  swrdrn3  32897  gsumzresunsn  33009  gsumhashmul  33014  tocycfv  33051  tocycf  33059  trsp2cyc  33065  cycpmco2f1  33066  cycpmco2rn  33067  cycpmconjvlem  33083  cycpmconjslem2  33097  qusbas2  33343  qusima  33345  qusrn  33346  nsgmgc  33349  nsgqusf1olem2  33351  idlsrgval  33440  algextdeglem4  33687  smatrcl  33763  ordtprsval  33885  ordtprsuni  33886  ordtcnvNEW  33887  ordtrestNEW  33888  ordtrest2NEW  33890  qqhval  33939  qqhval2  33949  esumval  34013  esumsnf  34031  esumrnmpt2  34035  esumfsupre  34038  esumsup  34056  sxval  34157  omsval  34261  omsfval  34262  carsggect  34286  sibf0  34302  sitgfval  34309  cvmlift3lem6  35297  satfrnmapom  35343  mvtval  35473  mvrsval  35478  mrsubvrs  35495  elmsubrn  35501  msubrn  35502  mstaval  35517  msubvrs  35533  mclsval  35536  filnetlem4  36355  mptsnunlem  37312  dissneqlem  37314  exrecfnlem  37353  ctbssinf  37380  poimirlem3  37603  poimirlem9  37609  poimirlem16  37616  poimirlem17  37617  poimirlem19  37619  poimirlem20  37620  poimirlem24  37624  poimirlem30  37630  poimirlem32  37632  mblfinlem2  37638  ovoliunnfl  37642  voliunnfl  37644  isrngo  37877  drngoi  37931  rngohomval  37944  rngoisoval  37957  idlval  37993  pridlval  38013  maxidlval  38019  igenval  38041  cnvref4  38318  symrelim  38536  unidmqs  38632  lsatset  38969  docaffvalN  41100  docafvalN  41101  aks6d1c2  42103  sticksstones2  42120  sticksstones3  42121  qsalrel  42213  prjcrvfval  42604  mzpmfp  42720  eldiophb  42730  diophrw  42732  tfsconcatrn  43315  rp-tfslim  43326  conrel1d  43636  iunrelexp0  43675  rntrclfv  43705  clsneibex  44075  neicvgbex  44085  rnsnf  45162  fsneqrn  45189  limsupval3  45673  limsupresre  45677  limsupresico  45681  limsuppnfdlem  45682  limsupvaluz  45689  limsupvaluzmpt  45698  limsupvaluz2  45719  supcnvlimsup  45721  supcnvlimsupmpt  45722  liminfval  45740  liminfval5  45746  limsupresxr  45747  liminfresxr  45748  liminfresico  45752  liminfvalxr  45764  fourierdlem60  46147  fourierdlem61  46148  sge0val  46347  sge0z  46356  sge0revalmpt  46359  sge0tsms  46361  sge0sup  46372  sge0split  46390  sge0fodjrnlem  46397  sge0seq  46427  meadjiunlem  46446  meaiuninclem  46461  omeiunle  46498  ovolval2lem  46624  ovolval4lem2  46631  ovolval5lem2  46634  ovolval5lem3  46635  ovolval5  46636  ovnovollem2  46638  smfsuplem2  46793  smfsup  46795  smfsupmpt  46796  smfinf  46799  smfinfmpt  46800  smflimsuplem1  46801  smflimsuplem2  46802  smflimsuplem4  46804  smflimsuplem5  46805  smflimsuplem7  46807  smflimsup  46809  fnrnafv  47146  afv2eq12d  47199  isubgredgss  47849  isubgredg  47850  stgredg  47940  gpgedg  48029  dmrnxp  48821  imaidfu  49095  idfudiag1lem  49508