Theorem rneqd 5891

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

Syntax hints:   → wi 4   = wceq 1540  ran crn 5632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  resima2  5976  elimampt  6003  imaeq1  6015  imaeq2  6016  mptimass  6033  resiima  6036  imadifssran  6112  rnxpid  6134  xpima  6143  funimacnv  6581  fnima  6630  focofo  6767  rnfvprc  6834  elimampo  7506  elxp4  7878  elxp5  7879  2ndval  7950  fo2nd  7968  f2ndres  7972  curry1  8060  curry2  8063  oarec  8503  en1  8972  xpassen  9012  xpdom2  9013  sbthlem4  9031  fodomr  9069  fodomfir  9255  dffi3  9358  marypha2lem4  9365  ordtypelem9  9455  dfac12lem1  10073  dfac12r  10076  fin23lem32  10273  fin23lem34  10275  fin23lem35  10276  fin23lem36  10277  fin23lem38  10278  fin23lem39  10279  fin23lem41  10281  itunitc  10350  ttukeylem3  10440  fpwwe2lem5  10564  fpwwe2lem8  10567  wunex2  10667  wuncval2  10676  gruima  10731  rpnnen1lem6  12917  hashf1lem1  14396  s1rn  14540  s2rn  14905  s3rn  14906  s7rn  14907  relexprng  14988  relexprnd  14990  relexpfld  14991  limsupval  15416  vdwapfval  16918  vdwapval  16920  vdwmc  16925  vdwpc  16927  vdwlem6  16933  vdwlem8  16935  restval  17365  restid2  17369  prdsval  17394  prdsdsval  17417  prdsdsval2  17423  prdsdsval3  17424  imasval  17450  imasdsval  17454  isfull  17854  arwval  17985  gsumvalx  18585  conjsubg  19164  psgnfval  19414  sylow1lem2  19513  sylow1lem4  19515  sylow1  19517  sylow2blem1  19534  sylow2b  19537  sylow3lem1  19541  sylow3lem2  19542  sylow3lem3  19543  sylow3lem5  19545  sylow3lem6  19546  sylow3  19547  lsmfval  19552  lsmvalx  19553  oppglsm  19556  subglsm  19587  lsmpropd  19591  efgval2  19638  efgi2  19639  efgtlen  19640  efgsdm  19644  efgsdmi  19646  efgsrel  19648  efgs1b  19650  efgsp1  19651  efgsres  19652  efgsfo  19653  efgrelexlemb  19664  frgpnabllem1  19787  iscyg  19793  iscyggen  19794  gsumxp  19890  dprdval  19919  ablfac2  20005  zncyg  21490  cygznlem2a  21509  frlmsplit2  21715  evlseu  22023  tgrest  23079  ordtval  23109  ordtbas2  23111  ordtcnv  23121  ordtrest  23122  ordtrest2  23124  ispnrm  23259  cmpfi  23328  txval  23484  xkoval  23507  ptval2  23521  ptpjopn  23532  xkoccn  23539  xkoptsub  23574  xkopt  23575  fmval  23863  fmf  23865  txflf  23926  cnextf  23986  subgntr  24027  opnsubg  24028  clsnsg  24030  snclseqg  24036  tsmsval2  24050  tsmsxplem1  24073  ustuqtoplem  24160  utopsnneiplem  24168  utopsnneip  24169  fmucndlem  24211  ressprdsds  24292  mopnval  24359  metuval  24470  metdsval  24769  lebnumlem1  24893  lebnumlem3  24895  pi1xfrcnvlem  24989  pi1xfrcnv  24990  minveclem3b  25361  elovolmr  25410  ovolctb  25424  ovoliunlem3  25438  ovolshftlem1  25443  voliunlem3  25486  voliun  25488  volsup  25490  uniioombllem2  25517  uniioombllem3  25519  mbflimsup  25600  itg1climres  25648  itg2monolem1  25684  itg2i1fseq  25689  itg2cnlem1  25695  ellimc2  25811  dvivth  25948  dvne0  25949  lhop2  25953  lhop  25954  mdegfval  26000  dchrptlem2  27209  dchrpt  27211  seqsval  28222  om2noseqfo  28232  tglnunirn  28528  tgisline  28607  perpln1  28690  perpln2  28691  isperp  28692  ishpg  28739  lmif  28765  islmib  28767  edgval  29029  edgopval  29031  edgstruct  29033  uhgr2edg  29188  usgr1e  29225  cplgrop  29417  cusgrexi  29423  structtocusgr  29426  1loopgredg  29482  1egrvtxdg0  29492  umgr2v2eedg  29505  ex-ima  30421  bafval  30583  pj3i  32187  ofrn2  32614  ffsrn  32702  prodindf  32836  pfxrn2  32911  pfxrn3  32912  swrdrn2  32926  swrdrn3  32927  gsumzresunsn  33039  gsumhashmul  33044  tocycfv  33081  tocycf  33089  trsp2cyc  33095  cycpmco2f1  33096  cycpmco2rn  33097  cycpmconjvlem  33113  cycpmconjslem2  33127  qusbas2  33370  qusima  33372  qusrn  33373  nsgmgc  33376  nsgqusf1olem2  33378  idlsrgval  33467  algextdeglem4  33703  smatrcl  33779  ordtprsval  33901  ordtprsuni  33902  ordtcnvNEW  33903  ordtrestNEW  33904  ordtrest2NEW  33906  qqhval  33955  qqhval2  33965  esumval  34029  esumsnf  34047  esumrnmpt2  34051  esumfsupre  34054  esumsup  34072  sxval  34173  omsval  34277  omsfval  34278  carsggect  34302  sibf0  34318  sitgfval  34325  cvmlift3lem6  35304  satfrnmapom  35350  mvtval  35480  mvrsval  35485  mrsubvrs  35502  elmsubrn  35508  msubrn  35509  mstaval  35524  msubvrs  35540  mclsval  35543  filnetlem4  36362  mptsnunlem  37319  dissneqlem  37321  exrecfnlem  37360  ctbssinf  37387  poimirlem3  37610  poimirlem9  37616  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem24  37631  poimirlem30  37637  poimirlem32  37639  mblfinlem2  37645  ovoliunnfl  37649  voliunnfl  37651  isrngo  37884  drngoi  37938  rngohomval  37951  rngoisoval  37964  idlval  38000  pridlval  38020  maxidlval  38026  igenval  38048  cnvref4  38325  symrelim  38543  unidmqs  38639  lsatset  38976  docaffvalN  41108  docafvalN  41109  aks6d1c2  42111  sticksstones2  42128  sticksstones3  42129  qsalrel  42221  prjcrvfval  42612  mzpmfp  42728  eldiophb  42738  diophrw  42740  tfsconcatrn  43324  rp-tfslim  43335  conrel1d  43645  iunrelexp0  43684  rntrclfv  43714  clsneibex  44084  neicvgbex  44094  rnsnf  45171  fsneqrn  45198  limsupval3  45683  limsupresre  45687  limsupresico  45691  limsuppnfdlem  45692  limsupvaluz  45699  limsupvaluzmpt  45708  limsupvaluz2  45729  supcnvlimsup  45731  supcnvlimsupmpt  45732  liminfval  45750  liminfval5  45756  limsupresxr  45757  liminfresxr  45758  liminfresico  45762  liminfvalxr  45774  fourierdlem60  46157  fourierdlem61  46158  sge0val  46357  sge0z  46366  sge0revalmpt  46369  sge0tsms  46371  sge0sup  46382  sge0split  46400  sge0fodjrnlem  46407  sge0seq  46437  meadjiunlem  46456  meaiuninclem  46471  omeiunle  46508  ovolval2lem  46634  ovolval4lem2  46641  ovolval5lem2  46644  ovolval5lem3  46645  ovolval5  46646  ovnovollem2  46648  smfsuplem2  46803  smfsup  46805  smfsupmpt  46806  smfinf  46809  smfinfmpt  46810  smflimsuplem1  46811  smflimsuplem2  46812  smflimsuplem4  46814  smflimsuplem5  46815  smflimsuplem7  46817  smflimsup  46819  fnrnafv  47156  afv2eq12d  47209  isubgredgss  47858  isubgredg  47859  stgredg  47948  gpgedg  48029  dmrnxp  48818  imaidfu  49092  idfudiag1lem  49505