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 1547  ran crn 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-cnv 5626  df-dm 5628  df-rn 5629

This theorem is referenced by:  resima2  5968  elimampt  5995  imaeq1  6007  imaeq2  6008  mptimass  6025  resiima  6028  imadifssran  6102  rnxpid  6124  xpima  6133  funimacnv  6566  fnima  6615  focofo  6752  rnfvprc  6821  elimampo  7493  elxp4  7862  elxp5  7863  2ndval  7934  fo2nd  7952  f2ndres  7956  curry1  8043  curry2  8046  oarec  8487  en1  8961  xpassen  8999  xpdom2  9000  sbthlem4  9018  fodomr  9056  fodomfir  9228  dffi3  9334  marypha2lem4  9341  ordtypelem9  9431  dfac12lem1  10057  dfac12r  10060  fin23lem32  10257  fin23lem34  10259  fin23lem35  10260  fin23lem36  10261  fin23lem38  10262  fin23lem39  10263  fin23lem41  10265  itunitc  10334  ttukeylem3  10424  fpwwe2lem5  10549  fpwwe2lem8  10552  wunex2  10652  wuncval2  10661  gruima  10716  rpnnen1lem6  12923  hashf1lem1  14408  s1rn  14553  s2rn  14916  s3rn  14917  s7rn  14918  relexprng  14999  relexprnd  15001  relexpfld  15002  limsupval  15427  vdwapfval  16933  vdwapval  16935  vdwmc  16940  vdwpc  16942  vdwlem6  16948  vdwlem8  16950  restval  17380  restid2  17384  prdsval  17409  prdsdsval  17432  prdsdsval2  17438  prdsdsval3  17439  imasval  17466  imasdsval  17470  isfull  17870  arwval  18001  gsumvalx  18635  conjsubg  19216  psgnfval  19466  sylow1lem2  19565  sylow1lem4  19567  sylow1  19569  sylow2blem1  19586  sylow2b  19589  sylow3lem1  19593  sylow3lem2  19594  sylow3lem3  19595  sylow3lem5  19597  sylow3lem6  19598  sylow3  19599  lsmfval  19604  lsmvalx  19605  oppglsm  19608  subglsm  19639  lsmpropd  19643  efgval2  19690  efgi2  19691  efgtlen  19692  efgsdm  19696  efgsdmi  19698  efgsrel  19700  efgs1b  19702  efgsp1  19703  efgsres  19704  efgsfo  19705  efgrelexlemb  19716  frgpnabllem1  19839  iscyg  19845  iscyggen  19846  gsumxp  19942  dprdval  19971  ablfac2  20057  zncyg  21523  cygznlem2a  21542  frlmsplit2  21748  evlseu  22059  tgrest  23142  ordtval  23172  ordtbas2  23174  ordtcnv  23184  ordtrest  23185  ordtrest2  23187  ispnrm  23322  cmpfi  23391  txval  23547  xkoval  23570  ptval2  23584  ptpjopn  23595  xkoccn  23602  xkoptsub  23637  xkopt  23638  fmval  23926  fmf  23928  txflf  23989  cnextf  24049  subgntr  24090  opnsubg  24091  clsnsg  24093  snclseqg  24099  tsmsval2  24113  tsmsxplem1  24136  ustuqtoplem  24222  utopsnneiplem  24230  utopsnneip  24231  fmucndlem  24273  ressprdsds  24354  mopnval  24421  metuval  24532  metdsval  24831  lebnumlem1  24946  lebnumlem3  24948  pi1xfrcnvlem  25041  pi1xfrcnv  25042  minveclem3b  25413  elovolmr  25461  ovolctb  25475  ovoliunlem3  25489  ovolshftlem1  25494  voliunlem3  25537  voliun  25539  volsup  25541  uniioombllem2  25568  uniioombllem3  25570  mbflimsup  25651  itg1climres  25699  itg2monolem1  25735  itg2i1fseq  25740  itg2cnlem1  25746  ellimc2  25862  dvivth  25995  dvne0  25996  lhop2  26000  lhop  26001  mdegfval  26045  dchrptlem2  27246  dchrpt  27248  seqsval  28298  om2noseqfo  28308  tglnunirn  28634  tgisline  28713  perpln1  28796  perpln2  28797  isperp  28798  ishpg  28845  lmif  28871  islmib  28873  edgval  29136  edgopval  29138  edgstruct  29140  uhgr2edg  29295  usgr1e  29332  cplgrop  29524  cusgrexi  29530  structtocusgr  29533  1loopgredg  29588  1egrvtxdg0  29598  umgr2v2eedg  29611  ex-ima  30530  bafval  30693  pj3i  32297  ofrn2  32732  rnressnsn  32769  ffsrn  32820  prodindf  32941  pfxrn2  33019  pfxrn3  33020  swrdrn2  33033  swrdrn3  33034  gsumzresunsn  33143  gsumhashmul  33148  tocycfv  33190  tocycf  33198  trsp2cyc  33204  cycpmco2f1  33205  cycpmco2rn  33206  cycpmconjvlem  33222  cycpmconjslem2  33236  domnprodeq0  33357  qusbas2  33489  qusima  33491  qusrn  33492  nsgmgc  33495  nsgqusf1olem2  33497  idlsrgval  33586  esplyfval1  33757  esplyfvaln  33758  esplyind  33759  algextdeglem4  33904  smatrcl  33980  ordtprsval  34102  ordtprsuni  34103  ordtcnvNEW  34104  ordtrestNEW  34105  ordtrest2NEW  34107  qqhval  34156  qqhval2  34166  esumval  34230  esumsnf  34248  esumrnmpt2  34252  esumfsupre  34255  esumsup  34273  sxval  34374  omsval  34477  omsfval  34478  carsggect  34502  sibf0  34518  sitgfval  34525  cvmlift3lem6  35552  satfrnmapom  35598  mvtval  35728  mvrsval  35733  mrsubvrs  35750  elmsubrn  35756  msubrn  35757  mstaval  35772  msubvrs  35788  mclsval  35791  filnetlem4  36609  mptsnunlem  37700  dissneqlem  37702  exrecfnlem  37741  ctbssinf  37768  poimirlem3  37990  poimirlem9  37996  poimirlem16  38003  poimirlem17  38004  poimirlem19  38006  poimirlem20  38007  poimirlem24  38011  poimirlem30  38017  poimirlem32  38019  mblfinlem2  38025  ovoliunnfl  38029  voliunnfl  38031  isrngo  38264  drngoi  38318  rngohomval  38331  rngoisoval  38344  idlval  38380  pridlval  38400  maxidlval  38406  igenval  38428  cnvref4  38717  symrelim  39010  unidmqs  39106  lsatset  39482  docaffvalN  41613  docafvalN  41614  aks6d1c2  42615  sticksstones2  42632  sticksstones3  42633  qsalrel  42725  prjcrvfval  43081  mzpmfp  43196  eldiophb  43206  diophrw  43208  tfsconcatrn  43787  rp-tfslim  43798  conrel1d  44107  iunrelexp0  44146  rntrclfv  44176  clsneibex  44546  neicvgbex  44556  rnsnf  45631  fsneqrn  45656  limsupval3  46135  limsupresre  46139  limsupresico  46143  limsuppnfdlem  46144  limsupvaluz  46151  limsupvaluzmpt  46160  limsupvaluz2  46181  supcnvlimsup  46183  supcnvlimsupmpt  46184  liminfval  46202  liminfval5  46208  limsupresxr  46209  liminfresxr  46210  liminfresico  46214  liminfvalxr  46226  fourierdlem60  46609  fourierdlem61  46610  sge0val  46809  sge0z  46818  sge0revalmpt  46821  sge0tsms  46823  sge0sup  46834  sge0split  46852  sge0fodjrnlem  46859  sge0seq  46889  meadjiunlem  46908  meaiuninclem  46923  omeiunle  46960  ovolval2lem  47086  ovolval4lem2  47093  ovolval5lem2  47096  ovolval5lem3  47097  ovolval5  47098  ovnovollem2  47100  smfsuplem2  47255  smfsup  47257  smfsupmpt  47258  smfinf  47261  smfinfmpt  47262  smflimsuplem1  47263  smflimsuplem2  47264  smflimsuplem4  47266  smflimsuplem5  47267  smflimsuplem7  47269  smflimsup  47271  fnrnafv  47625  afv2eq12d  47678  isubgredgss  48356  isubgredg  48357  stgredg  48447  gpgedg  48536  dmrnxp  49327  imaidfu  49600  idfudiag1lem  50013