Theorem rneqd 5930

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ran crn 5664

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-cnv 5671  df-dm 5673  df-rn 5674

This theorem is used by:  resima2  6017  elimampt  6047  imaeq1  6059  imaeq2  6060  mptimass  6077  resiima  6080  rnxpid  6173  xpima  6182  imadifssranOLD  6205  funimacnv  6621  fnima  6669  focofo  6809  rnfvprc  6879  elimampo  7556  elxp4  7925  elxp5  7926  2ndval  7995  fo2nd  8013  f2ndres  8017  curry1  8105  curry2  8108  oarec  8553  en1  9027  xpassen  9066  xpdom2  9067  sbthlem4  9085  fodomr  9123  fodomfir  9294  dffi3  9398  marypha2lem4  9405  ordtypelem9  9495  dfac12lem1  10143  dfac12r  10146  fin23lem32  10343  fin23lem34  10345  fin23lem35  10346  fin23lem36  10347  fin23lem38  10348  fin23lem39  10349  fin23lem41  10351  itunitc  10420  ttukeylem3  10510  fpwwe2lem5  10635  fpwwe2lem8  10638  wunex2  10738  wuncval2  10747  gruima  10802  rpnnen1lem6  13022  hashf1lem1  14510  s1rn  14656  swrdrn3  14712  s2rn  15024  s3rn  15025  s7rn  15026  relexprng  15107  relexprnd  15109  relexpfld  15110  limsupval  15549  vdwapfval  17053  vdwapval  17055  vdwmc  17060  vdwpc  17062  vdwlem6  17068  vdwlem8  17070  restval  17501  restid2  17505  prdsval  17530  prdsdsval  17553  prdsdsval2  17559  prdsdsval3  17560  imasval  17587  imasdsval  17591  isfull  17991  arwval  18122  gsumvalx  18766  conjsubg  19364  psgnfval  19614  sylow1lem2  19713  sylow1lem4  19715  sylow1  19717  sylow2blem1  19734  sylow2b  19737  sylow3lem1  19741  sylow3lem2  19742  sylow3lem3  19743  sylow3lem5  19745  sylow3lem6  19746  sylow3  19747  lsmfval  19752  lsmvalx  19753  oppglsm  19756  subglsm  19787  lsmpropd  19791  efgval2  19838  efgi2  19839  efgtlen  19840  efgsdm  19844  efgsdmi  19846  efgsrel  19848  efgs1b  19850  efgsp1  19851  efgsres  19852  efgsfo  19853  efgrelexlemb  19864  frgpnabllem1  19987  iscyg  19993  iscyggen  19994  gsumxp  20090  dprdval  20119  ablfac2  20205  zncyg  21748  cygznlem2a  21767  frlmsplit2  21973  evlseu  22284  tgrest  23366  ordtval  23396  ordtbas2  23398  ordtcnv  23408  ordtrest  23409  ordtrest2  23411  ispnrm  23546  cmpfi  23615  txval  23772  xkoval  23795  ptval2  23809  ptpjopn  23820  xkoccn  23827  xkoptsub  23862  xkopt  23863  fmval  24151  fmf  24153  txflf  24214  cnextf  24274  subgntr  24315  opnsubg  24316  clsnsg  24318  snclseqg  24324  tsmsval2  24338  tsmsxplem1  24361  ustuqtoplem  24447  utopsnneiplem  24455  utopsnneip  24456  fmucndlem  24498  ressprdsds  24579  mopnval  24646  metuval  24757  metdsval  25056  lebnumlem1  25171  lebnumlem3  25173  pi1xfrcnvlem  25266  pi1xfrcnv  25267  minveclem3b  25638  elovolmr  25686  ovolctb  25700  ovoliunlem3  25714  ovolshftlem1  25719  voliunlem3  25762  voliun  25764  volsup  25766  uniioombllem2  25793  uniioombllem3  25795  mbflimsup  25876  itg1climres  25924  itg2monolem1  25960  itg2i1fseq  25965  itg2cnlem1  25971  ellimc2  26087  dvivth  26220  dvne0  26221  lhop2  26225  lhop  26226  mdegfval  26270  dchrptlem2  27480  dchrpt  27482  seqsval  28532  om2noseqfo  28542  tglnunirn  28868  tgisline  28951  perpln1  29041  perpln2  29042  isperp  29043  ishpg  29092  tgplnfn  29108  plngval  29110  isplng  29111  lmif  29145  islmib  29147  brprlng  29243  edgval  29454  edgopval  29456  edgstruct  29458  uhgr2edg  29616  usgr1e  29653  cplgrop  29845  cusgrexi  29851  structtocusgr  29854  1loopgredg  29909  1egrvtxdg0  29919  umgr2v2eedg  29932  ex-ima  30864  bafval  31027  pj3i  32631  ofrn2  33056  rnressnsn  33093  ffsrn  33143  prodindf  33252  pfxrn2  33330  pfxrn3  33331  swrdrn2  33340  gsumzresunsn  33446  gsumhashmul  33451  tocycfv  33493  tocycf  33501  trsp2cyc  33507  cycpmco2f1  33508  cycpmco2rn  33509  cycpmconjvlem  33525  cycpmconjslem2  33539  domnprodeq0  33663  qusbas2  33779  qusima  33781  qusrn  33782  nsgmgc  33785  nsgqusf1olem2  33787  idlsrgval  33857  esplyfval1  34027  esplyfvaln  34028  esplyind  34029  algextdeglem4  34174  smatrcl  34250  ordtprsval  34372  ordtprsuni  34373  ordtcnvNEW  34374  ordtrestNEW  34375  ordtrest2NEW  34377  qqhval  34426  qqhval2  34436  esumval  34500  esumsnf  34518  esumrnmpt2  34522  esumfsupre  34525  esumsup  34543  sxval  34645  omsval  34748  omsfval  34749  carsggect  34773  sibf0  34789  sitgfval  34796  cvmlift3lem6  35853  satfrnmapom  35899  mvtval  36029  mvrsval  36034  mrsubvrs  36051  elmsubrn  36057  msubrn  36058  mstaval  36073  msubvrs  36089  mclsval  36092  filnetlem4  36949  mptsnunlem  38041  dissneqlem  38043  exrecfnlem  38082  ctbssinf  38109  poimirlem3  38331  poimirlem9  38337  poimirlem16  38344  poimirlem17  38345  poimirlem19  38347  poimirlem20  38348  poimirlem24  38352  poimirlem30  38358  poimirlem32  38360  mblfinlem2  38366  ovoliunnfl  38370  voliunnfl  38372  isrngo  38606  drngoi  38660  rngohomval  38673  rngoisoval  38686  idlval  38722  pridlval  38742  maxidlval  38748  igenval  38770  cnvref4  39057  symrelim  39350  unidmqs  39446  lsatset  39822  docaffvalN  41953  docafvalN  41954  aks6d1c2  42955  sticksstones2  42972  sticksstones3  42973  qsalrel  43067  prjcrvfval  43421  mzpmfp  43536  eldiophb  43546  diophrw  43548  tfsconcatrn  44127  rp-tfslim  44138  conrel1d  44447  iunrelexp0  44486  rntrclfv  44516  clsneibex  44886  neicvgbex  44896  rnsnf  45960  fsneqrn  45985  limsupval3  46464  limsupresre  46468  limsupresico  46472  limsuppnfdlem  46473  limsupvaluz  46480  limsupvaluzmpt  46489  limsupvaluz2  46510  supcnvlimsup  46512  supcnvlimsupmpt  46513  liminfval  46531  liminfval5  46537  limsupresxr  46538  liminfresxr  46539  liminfresico  46543  liminfvalxr  46555  fourierdlem60  46938  fourierdlem61  46939  sge0val  47138  sge0z  47147  sge0revalmpt  47150  sge0tsms  47152  sge0sup  47163  sge0split  47181  sge0fodjrnlem  47188  sge0seq  47218  meadjiunlem  47237  meaiuninclem  47252  omeiunle  47289  ovolval2lem  47415  ovolval4lem2  47422  ovolval5lem2  47425  ovolval5lem3  47426  ovolval5  47427  ovnovollem2  47429  smfsuplem2  47584  smfsup  47586  smfsupmpt  47587  smfinf  47590  smfinfmpt  47591  smflimsuplem1  47592  smflimsuplem2  47593  smflimsuplem4  47595  smflimsuplem5  47596  smflimsuplem7  47598  smflimsup  47600  fnrnafv  47957  afv2eq12d  48010  isubgredgss  48688  isubgredg  48689  stgredg  48779  gpgedg  48868  dmrnxp  49672  imaidfu  49945  idfudiag1lem  50358