Theorem rneqd 5929

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

Syntax hints:   → wi 4   = wceq 1567  ran crn 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-cnv 5670  df-dm 5672  df-rn 5673

This theorem is referenced by:  resima2  6016  elimampt  6046  imaeq1  6058  imaeq2  6059  mptimass  6076  resiima  6079  rnxpid  6172  xpima  6181  imadifssranOLD  6204  funimacnv  6618  fnima  6666  focofo  6806  rnfvprc  6876  elimampo  7548  elxp4  7918  elxp5  7919  2ndval  7988  fo2nd  8006  f2ndres  8010  curry1  8098  curry2  8101  oarec  8546  en1  9020  xpassen  9058  xpdom2  9059  sbthlem4  9077  fodomr  9115  fodomfir  9286  dffi3  9390  marypha2lem4  9397  ordtypelem9  9487  dfac12lem1  10126  dfac12r  10129  fin23lem32  10327  fin23lem34  10329  fin23lem35  10330  fin23lem36  10331  fin23lem38  10332  fin23lem39  10333  fin23lem41  10335  itunitc  10404  ttukeylem3  10494  fpwwe2lem5  10619  fpwwe2lem8  10622  wunex2  10722  wuncval2  10731  gruima  10786  rpnnen1lem6  13005  hashf1lem1  14491  s1rn  14636  s2rn  14999  s3rn  15000  s7rn  15001  relexprng  15082  relexprnd  15084  relexpfld  15085  limsupval  15524  vdwapfval  17030  vdwapval  17032  vdwmc  17037  vdwpc  17039  vdwlem6  17045  vdwlem8  17047  restval  17478  restid2  17482  prdsval  17507  prdsdsval  17530  prdsdsval2  17536  prdsdsval3  17537  imasval  17564  imasdsval  17568  isfull  17968  arwval  18099  gsumvalx  18733  conjsubg  19319  psgnfval  19569  sylow1lem2  19668  sylow1lem4  19670  sylow1  19672  sylow2blem1  19689  sylow2b  19692  sylow3lem1  19696  sylow3lem2  19697  sylow3lem3  19698  sylow3lem5  19700  sylow3lem6  19701  sylow3  19702  lsmfval  19707  lsmvalx  19708  oppglsm  19711  subglsm  19742  lsmpropd  19746  efgval2  19793  efgi2  19794  efgtlen  19795  efgsdm  19799  efgsdmi  19801  efgsrel  19803  efgs1b  19805  efgsp1  19806  efgsres  19807  efgsfo  19808  efgrelexlemb  19819  frgpnabllem1  19942  iscyg  19948  iscyggen  19949  gsumxp  20045  dprdval  20074  ablfac2  20160  zncyg  21666  cygznlem2a  21685  frlmsplit2  21891  evlseu  22202  tgrest  23284  ordtval  23314  ordtbas2  23316  ordtcnv  23326  ordtrest  23327  ordtrest2  23329  ispnrm  23464  cmpfi  23533  txval  23689  xkoval  23712  ptval2  23726  ptpjopn  23737  xkoccn  23744  xkoptsub  23779  xkopt  23780  fmval  24068  fmf  24070  txflf  24131  cnextf  24191  subgntr  24232  opnsubg  24233  clsnsg  24235  snclseqg  24241  tsmsval2  24255  tsmsxplem1  24278  ustuqtoplem  24364  utopsnneiplem  24372  utopsnneip  24373  fmucndlem  24415  ressprdsds  24496  mopnval  24563  metuval  24674  metdsval  24973  lebnumlem1  25088  lebnumlem3  25090  pi1xfrcnvlem  25183  pi1xfrcnv  25184  minveclem3b  25555  elovolmr  25603  ovolctb  25617  ovoliunlem3  25631  ovolshftlem1  25636  voliunlem3  25679  voliun  25681  volsup  25683  uniioombllem2  25710  uniioombllem3  25712  mbflimsup  25793  itg1climres  25841  itg2monolem1  25877  itg2i1fseq  25882  itg2cnlem1  25888  ellimc2  26004  dvivth  26137  dvne0  26138  lhop2  26142  lhop  26143  mdegfval  26187  dchrptlem2  27394  dchrpt  27396  seqsval  28446  om2noseqfo  28456  tglnunirn  28782  tgisline  28861  perpln1  28948  perpln2  28949  isperp  28950  ishpg  28999  tgplnfn  29014  plngval  29016  isplng  29017  lmif  29051  islmib  29053  brprlng  29142  edgval  29339  edgopval  29341  edgstruct  29343  uhgr2edg  29498  usgr1e  29535  cplgrop  29727  cusgrexi  29733  structtocusgr  29736  1loopgredg  29791  1egrvtxdg0  29801  umgr2v2eedg  29814  ex-ima  30733  bafval  30896  pj3i  32500  ofrn2  32925  rnressnsn  32962  ffsrn  33013  prodindf  33122  pfxrn2  33200  pfxrn3  33201  swrdrn2  33214  swrdrn3  33215  gsumzresunsn  33322  gsumhashmul  33327  tocycfv  33369  tocycf  33377  trsp2cyc  33383  cycpmco2f1  33384  cycpmco2rn  33385  cycpmconjvlem  33401  cycpmconjslem2  33415  domnprodeq0  33539  qusbas2  33658  qusima  33660  qusrn  33661  nsgmgc  33664  nsgqusf1olem2  33666  idlsrgval  33737  esplyfval1  33907  esplyfvaln  33908  esplyind  33909  algextdeglem4  34054  smatrcl  34130  ordtprsval  34252  ordtprsuni  34253  ordtcnvNEW  34254  ordtrestNEW  34255  ordtrest2NEW  34257  qqhval  34306  qqhval2  34316  esumval  34380  esumsnf  34398  esumrnmpt2  34402  esumfsupre  34405  esumsup  34423  sxval  34524  omsval  34627  omsfval  34628  carsggect  34652  sibf0  34668  sitgfval  34675  cvmlift3lem6  35714  satfrnmapom  35760  mvtval  35890  mvrsval  35895  mrsubvrs  35912  elmsubrn  35918  msubrn  35919  mstaval  35934  msubvrs  35950  mclsval  35953  filnetlem4  36780  mptsnunlem  37871  dissneqlem  37873  exrecfnlem  37912  ctbssinf  37939  poimirlem3  38161  poimirlem9  38167  poimirlem16  38174  poimirlem17  38175  poimirlem19  38177  poimirlem20  38178  poimirlem24  38182  poimirlem30  38188  poimirlem32  38190  mblfinlem2  38196  ovoliunnfl  38200  voliunnfl  38202  isrngo  38435  drngoi  38489  rngohomval  38502  rngoisoval  38515  idlval  38551  pridlval  38571  maxidlval  38577  igenval  38599  cnvref4  38888  symrelim  39181  unidmqs  39277  lsatset  39653  docaffvalN  41784  docafvalN  41785  aks6d1c2  42786  sticksstones2  42803  sticksstones3  42804  qsalrel  42898  prjcrvfval  43254  mzpmfp  43369  eldiophb  43379  diophrw  43381  tfsconcatrn  43960  rp-tfslim  43971  conrel1d  44280  iunrelexp0  44319  rntrclfv  44349  clsneibex  44719  neicvgbex  44729  rnsnf  45793  fsneqrn  45818  limsupval3  46297  limsupresre  46301  limsupresico  46305  limsuppnfdlem  46306  limsupvaluz  46313  limsupvaluzmpt  46322  limsupvaluz2  46343  supcnvlimsup  46345  supcnvlimsupmpt  46346  liminfval  46364  liminfval5  46370  limsupresxr  46371  liminfresxr  46372  liminfresico  46376  liminfvalxr  46388  fourierdlem60  46771  fourierdlem61  46772  sge0val  46971  sge0z  46980  sge0revalmpt  46983  sge0tsms  46985  sge0sup  46996  sge0split  47014  sge0fodjrnlem  47021  sge0seq  47051  meadjiunlem  47070  meaiuninclem  47085  omeiunle  47122  ovolval2lem  47248  ovolval4lem2  47255  ovolval5lem2  47258  ovolval5lem3  47259  ovolval5  47260  ovnovollem2  47262  smfsuplem2  47417  smfsup  47419  smfsupmpt  47420  smfinf  47423  smfinfmpt  47424  smflimsuplem1  47425  smflimsuplem2  47426  smflimsuplem4  47428  smflimsuplem5  47429  smflimsuplem7  47431  smflimsup  47433  fnrnafv  47787  afv2eq12d  47840  isubgredgss  48518  isubgredg  48519  stgredg  48609  gpgedg  48698  dmrnxp  49499  imaidfu  49772  idfudiag1lem  50185