Theorem rneqd 5938

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

Syntax hints:   → wi 4   = wceq 1542  ran crn 5678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-cnv 5685  df-dm 5687  df-rn 5688

This theorem is referenced by:  resima2  6017  imaeq1  6055  imaeq2  6056  mptimass  6073  resiima  6076  rnxpid  6173  xpima  6182  funimacnv  6630  fnima  6681  focofo  6819  rnfvprc  6886  elxp4  7913  elxp5  7914  2ndval  7978  fo2nd  7996  f2ndres  8000  curry1  8090  curry2  8093  oarec  8562  en1  9021  en1OLD  9022  xpassen  9066  xpdom2  9067  sbthlem4  9086  fodomr  9128  dffi3  9426  marypha2lem4  9433  ordtypelem9  9521  dfac12lem1  10138  dfac12r  10141  fin23lem32  10339  fin23lem34  10341  fin23lem35  10342  fin23lem36  10343  fin23lem38  10344  fin23lem39  10345  fin23lem41  10347  itunitc  10416  ttukeylem3  10506  fpwwe2lem5  10630  fpwwe2lem8  10633  wunex2  10733  wuncval2  10742  gruima  10797  rpnnen1lem6  12966  hashf1lem1  14415  hashf1lem1OLD  14416  s1rn  14549  relexprng  14993  relexprnd  14995  relexpfld  14996  limsupval  15418  vdwapfval  16904  vdwapval  16906  vdwmc  16911  vdwpc  16913  vdwlem6  16919  vdwlem8  16921  restval  17372  restid2  17376  prdsval  17401  prdsdsval  17424  prdsdsval2  17430  prdsdsval3  17431  imasval  17457  imasdsval  17461  isfull  17861  arwval  17993  gsumvalx  18595  conjsubg  19124  psgnfval  19368  sylow1lem2  19467  sylow1lem4  19469  sylow1  19471  sylow2blem1  19488  sylow2b  19491  sylow3lem1  19495  sylow3lem2  19496  sylow3lem3  19497  sylow3lem5  19499  sylow3lem6  19500  sylow3  19501  lsmfval  19506  lsmvalx  19507  oppglsm  19510  subglsm  19541  lsmpropd  19545  efgval2  19592  efgi2  19593  efgtlen  19594  efgsdm  19598  efgsdmi  19600  efgsrel  19602  efgs1b  19604  efgsp1  19605  efgsres  19606  efgsfo  19607  efgrelexlemb  19618  frgpnabllem1  19741  iscyg  19747  iscyggen  19748  gsumxp  19844  dprdval  19873  ablfac2  19959  rnrhmsubrg  20352  zncyg  21104  cygznlem2a  21123  frlmsplit2  21328  evlseu  21646  tgrest  22663  ordtval  22693  ordtbas2  22695  ordtcnv  22705  ordtrest  22706  ordtrest2  22708  ispnrm  22843  cmpfi  22912  txval  23068  xkoval  23091  ptval2  23105  ptpjopn  23116  xkoccn  23123  xkoptsub  23158  xkopt  23159  fmval  23447  fmf  23449  txflf  23510  cnextf  23570  subgntr  23611  opnsubg  23612  clsnsg  23614  snclseqg  23620  tsmsval2  23634  tsmsxplem1  23657  ustuqtoplem  23744  utopsnneiplem  23752  utopsnneip  23753  fmucndlem  23796  ressprdsds  23877  mopnval  23944  metuval  24058  metdsval  24363  lebnumlem1  24477  lebnumlem3  24479  pi1xfrcnvlem  24572  pi1xfrcnv  24573  minveclem3b  24945  elovolmr  24993  ovolctb  25007  ovoliunlem3  25021  ovolshftlem1  25026  voliunlem3  25069  voliun  25071  volsup  25073  uniioombllem2  25100  uniioombllem3  25102  mbflimsup  25183  itg1climres  25232  itg2monolem1  25268  itg2i1fseq  25273  itg2cnlem1  25279  ellimc2  25394  dvivth  25527  dvne0  25528  lhop2  25532  lhop  25533  mdegfval  25580  dchrptlem2  26768  dchrpt  26770  tglnunirn  27799  tgisline  27878  perpln1  27961  perpln2  27962  isperp  27963  ishpg  28010  lmif  28036  islmib  28038  edgval  28309  edgopval  28311  edgstruct  28313  uhgr2edg  28465  usgr1e  28502  cplgrop  28694  cusgrexi  28700  structtocusgr  28703  1loopgredg  28758  1egrvtxdg0  28768  umgr2v2eedg  28781  ex-ima  29695  bafval  29857  pj3i  31461  elimampt  31862  ofrn2  31865  ffsrn  31954  pfxrn2  32106  pfxrn3  32107  swrdrn2  32118  swrdrn3  32119  gsumzresunsn  32206  gsumhashmul  32208  tocycfv  32268  tocycf  32276  trsp2cyc  32282  cycpmco2f1  32283  cycpmco2rn  32284  cycpmconjvlem  32300  cycpmconjslem2  32314  qusbas2  32517  qusima  32519  qusrn  32520  nsgmgc  32523  nsgqusf1olem2  32525  idlsrgval  32617  algextdeglem1  32772  smatrcl  32776  ordtprsval  32898  ordtprsuni  32899  ordtcnvNEW  32900  ordtrestNEW  32901  ordtrest2NEW  32903  qqhval  32954  qqhval2  32962  prodindf  33021  esumval  33044  esumsnf  33062  esumrnmpt2  33066  esumfsupre  33069  esumsup  33087  sxval  33188  omsval  33292  omsfval  33293  carsggect  33317  sibf0  33333  sitgfval  33340  cvmlift3lem6  34315  satfrnmapom  34361  mvtval  34491  mvrsval  34496  mrsubvrs  34513  elmsubrn  34519  msubrn  34520  mstaval  34535  msubvrs  34551  mclsval  34554  filnetlem4  35266  mptsnunlem  36219  dissneqlem  36221  exrecfnlem  36260  ctbssinf  36287  poimirlem3  36491  poimirlem9  36497  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem24  36512  poimirlem30  36518  poimirlem32  36520  mblfinlem2  36526  ovoliunnfl  36530  voliunnfl  36532  isrngo  36765  drngoi  36819  rngohomval  36832  rngoisoval  36845  idlval  36881  pridlval  36901  maxidlval  36907  igenval  36929  cnvref4  37219  symrelim  37429  unidmqs  37524  lsatset  37860  docaffvalN  39992  docafvalN  39993  sticksstones2  40963  sticksstones3  40964  qsalrel  41062  prjcrvfval  41373  mzpmfp  41485  eldiophb  41495  diophrw  41497  tfsconcatrn  42092  rp-tfslim  42103  conrel1d  42414  iunrelexp0  42453  rntrclfv  42483  clsneibex  42853  neicvgbex  42863  rnsnf  43881  fsneqrn  43910  limsupval3  44408  limsupresre  44412  limsupresico  44416  limsuppnfdlem  44417  limsupvaluz  44424  limsupvaluzmpt  44433  limsupvaluz2  44454  supcnvlimsup  44456  supcnvlimsupmpt  44457  liminfval  44475  liminfval5  44481  limsupresxr  44482  liminfresxr  44483  liminfresico  44487  liminfvalxr  44499  fourierdlem60  44882  fourierdlem61  44883  sge0val  45082  sge0z  45091  sge0revalmpt  45094  sge0tsms  45096  sge0sup  45107  sge0split  45125  sge0fodjrnlem  45132  sge0seq  45162  meadjiunlem  45181  meaiuninclem  45196  omeiunle  45233  ovolval2lem  45359  ovolval4lem2  45366  ovolval5lem2  45369  ovolval5lem3  45370  ovolval5  45371  ovnovollem2  45373  smfsuplem2  45528  smfsup  45530  smfsupmpt  45531  smfinf  45534  smfinfmpt  45535  smflimsuplem1  45536  smflimsuplem2  45537  smflimsuplem4  45539  smflimsuplem5  45540  smflimsuplem7  45542  smflimsup  45544  fnrnafv  45870  afv2eq12d  45923