Theorem rneqd 5600

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

Syntax hints:   → wi 4   = wceq 1601  ran crn 5358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4889  df-opab 4951  df-cnv 5365  df-dm 5367  df-rn 5368

This theorem is referenced by:  resima2  5683  imaeq1  5717  imaeq2  5718  resiima  5736  rnxpid  5823  xpima  5832  funimacnv  6217  fnima  6258  rnfvprc  6442  elxp4  7391  elxp5  7392  2ndval  7450  fo2nd  7468  f2ndres  7472  curry1  7552  curry2  7555  oarec  7928  en1  8310  xpassen  8344  xpdom2  8345  sbthlem4  8363  fodomr  8401  dffi3  8627  marypha2lem4  8634  ordtypelem9  8722  dfac12lem1  9302  dfac12r  9305  fin23lem32  9503  fin23lem34  9505  fin23lem35  9506  fin23lem36  9507  fin23lem38  9508  fin23lem39  9509  fin23lem41  9511  itunitc  9580  ttukeylem3  9670  fpwwe2lem6  9794  fpwwe2lem9  9797  wunex2  9897  wuncval2  9906  gruima  9961  rpnnen1lem6  12134  hashf1lem1  13559  s1rn  13695  relexprng  14199  relexpfld  14202  limsupval  14622  vdwapfval  16090  vdwapval  16092  vdwmc  16097  vdwpc  16099  vdwlem6  16105  vdwlem8  16107  restval  16484  restid2  16488  prdsval  16512  prdsdsval  16535  prdsdsval2  16541  prdsdsval3  16542  imasval  16568  imasdsval  16572  isfull  16966  arwval  17089  gsumvalx  17667  conjsubg  18087  psgnfval  18315  sylow1lem2  18409  sylow1lem4  18411  sylow1  18413  sylow2blem1  18430  sylow2b  18433  sylow3lem1  18437  sylow3lem2  18438  sylow3lem3  18439  sylow3lem5  18441  sylow3lem6  18442  sylow3  18443  lsmfval  18448  lsmvalx  18449  oppglsm  18452  subglsm  18481  lsmpropd  18485  efgval2  18532  efgi2  18533  efgtlen  18534  efgsdm  18538  efgsdmi  18540  efgsrel  18542  efgs1b  18544  efgsp1  18545  efgsres  18546  efgsresOLD  18547  efgsfo  18548  efgrelexlemb  18560  frgpnabllem1  18673  iscyg  18678  iscyggen  18679  gsumxp  18772  dprdval  18800  ablfac2  18886  evlseu  19923  zncyg  20303  cygznlem2a  20322  frlmsplit2  20527  tgrest  21382  ordtval  21412  ordtbas2  21414  ordtcnv  21424  ordtrest  21425  ordtrest2  21427  ispnrm  21562  cmpfi  21631  txval  21787  xkoval  21810  ptval2  21824  ptpjopn  21835  xkoccn  21842  xkoptsub  21877  xkopt  21878  fmval  22166  fmf  22168  txflf  22229  cnextf  22289  subgntr  22329  opnsubg  22330  clsnsg  22332  snclseqg  22338  tsmsval2  22352  tsmsxplem1  22375  ustuqtoplem  22462  utopsnneiplem  22470  utopsnneip  22471  fmucndlem  22514  ressprdsds  22595  mopnval  22662  metuval  22773  metdsval  23069  lebnumlem1  23179  lebnumlem3  23181  pi1xfrcnvlem  23274  pi1xfrcnv  23275  minveclem3b  23645  elovolmr  23691  ovolctb  23705  ovoliunlem3  23719  ovolshftlem1  23724  voliunlem3  23767  voliun  23769  volsup  23771  uniioombllem2  23798  uniioombllem3  23800  mbflimsup  23881  itg1climres  23929  itg2monolem1  23965  itg2i1fseq  23970  itg2cnlem1  23976  ellimc2  24089  dvivth  24221  dvne0  24222  lhop2  24226  lhop  24227  mdegfval  24270  dchrptlem2  25453  dchrpt  25455  tglnunirn  25916  tgisline  25995  perpln1  26078  perpln2  26079  isperp  26080  ishpg  26124  lmif  26150  islmib  26152  edgval  26414  edgopval  26416  edgstruct  26418  uhgr2edg  26571  usgr1e  26609  cplgrop  26802  cusgrexi  26808  structtocusgr  26811  1loopgredg  26866  1egrvtxdg0  26876  umgr2v2eedg  26889  ex-ima  27891  bafval  28048  pj3i  29656  elimampt  30020  ofrn2  30024  ffsrn  30087  smatrcl  30468  ordtprsval  30570  ordtprsuni  30571  ordtcnvNEW  30572  ordtrestNEW  30573  ordtrest2NEW  30575  qqhval  30624  qqhval2  30632  prodindf  30691  esumval  30714  esumsnf  30732  esumrnmpt2  30736  esumfsupre  30739  esumsup  30757  sxval  30859  omsval  30961  omsfval  30962  carsggect  30986  sibf0  31002  sitgfval  31009  cvmlift3lem6  31913  mvtval  32004  mvrsval  32009  mrsubvrs  32026  elmsubrn  32032  msubrn  32033  mstaval  32048  msubvrs  32064  mclsval  32067  trpredeq1  32316  trpredeq2  32317  trpredeq3  32318  filnetlem4  32972  mptsnunlem  33788  dissneqlem  33790  poimirlem3  34047  poimirlem9  34053  poimirlem16  34060  poimirlem17  34061  poimirlem19  34063  poimirlem20  34064  poimirlem24  34068  poimirlem30  34074  poimirlem32  34076  mblfinlem2  34082  ovoliunnfl  34086  voliunnfl  34088  isrngo  34329  drngoi  34383  rngohomval  34396  rngoisoval  34409  idlval  34445  pridlval  34465  maxidlval  34471  igenval  34493  symrelim  34942  lsatset  35153  docaffvalN  37284  docafvalN  37285  mzpmfp  38284  eldiophb  38294  diophrw  38296  conrel1d  38926  iunrelexp0  38965  rntrclfv  38995  clsneibex  39370  neicvgbex  39380  rnsnf  40307  fsneqrn  40338  mptima2  40384  limsupval3  40846  limsupresre  40850  limsupresico  40854  limsuppnfdlem  40855  limsupvaluz  40862  limsupvaluzmpt  40871  limsupvaluz2  40892  supcnvlimsup  40894  supcnvlimsupmpt  40895  liminfval  40913  liminfval5  40919  limsupresxr  40920  liminfresxr  40921  liminfresico  40925  liminfvalxr  40937  fourierdlem60  41324  fourierdlem61  41325  sge0val  41521  sge0z  41530  sge0revalmpt  41533  sge0tsms  41535  sge0sup  41546  sge0split  41564  sge0fodjrnlem  41571  sge0seq  41601  meadjiunlem  41620  meaiuninclem  41635  omeiunle  41672  ovolval2lem  41798  ovolval4lem2  41805  ovolval5lem2  41808  ovolval5lem3  41809  ovolval5  41810  ovnovollem2  41812  smfsuplem2  41959  smfsup  41961  smfsupmpt  41962  smfinf  41965  smfinfmpt  41966  smflimsuplem1  41967  smflimsuplem2  41968  smflimsuplem4  41970  smflimsuplem5  41971  smflimsuplem7  41973  smflimsup  41975  fnrnafv  42217  afv2eq12d  42270