Theorem rneqd 5877

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

Syntax hints:   → wi 4   = wceq 1541  ran crn 5615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-opab 5152  df-cnv 5622  df-dm 5624  df-rn 5625

This theorem is referenced by:  resima2  5964  elimampt  5991  imaeq1  6003  imaeq2  6004  mptimass  6021  resiima  6024  imadifssran  6098  rnxpid  6120  xpima  6129  funimacnv  6562  fnima  6611  focofo  6748  rnfvprc  6816  elimampo  7483  elxp4  7852  elxp5  7853  2ndval  7924  fo2nd  7942  f2ndres  7946  curry1  8034  curry2  8037  oarec  8477  en1  8946  xpassen  8984  xpdom2  8985  sbthlem4  9003  fodomr  9041  fodomfir  9212  dffi3  9315  marypha2lem4  9322  ordtypelem9  9412  dfac12lem1  10035  dfac12r  10038  fin23lem32  10235  fin23lem34  10237  fin23lem35  10238  fin23lem36  10239  fin23lem38  10240  fin23lem39  10241  fin23lem41  10243  itunitc  10312  ttukeylem3  10402  fpwwe2lem5  10526  fpwwe2lem8  10529  wunex2  10629  wuncval2  10638  gruima  10693  rpnnen1lem6  12880  hashf1lem1  14362  s1rn  14507  s2rn  14870  s3rn  14871  s7rn  14872  relexprng  14953  relexprnd  14955  relexpfld  14956  limsupval  15381  vdwapfval  16883  vdwapval  16885  vdwmc  16890  vdwpc  16892  vdwlem6  16898  vdwlem8  16900  restval  17330  restid2  17334  prdsval  17359  prdsdsval  17382  prdsdsval2  17388  prdsdsval3  17389  imasval  17415  imasdsval  17419  isfull  17819  arwval  17950  gsumvalx  18584  conjsubg  19162  psgnfval  19412  sylow1lem2  19511  sylow1lem4  19513  sylow1  19515  sylow2blem1  19532  sylow2b  19535  sylow3lem1  19539  sylow3lem2  19540  sylow3lem3  19541  sylow3lem5  19543  sylow3lem6  19544  sylow3  19545  lsmfval  19550  lsmvalx  19551  oppglsm  19554  subglsm  19585  lsmpropd  19589  efgval2  19636  efgi2  19637  efgtlen  19638  efgsdm  19642  efgsdmi  19644  efgsrel  19646  efgs1b  19648  efgsp1  19649  efgsres  19650  efgsfo  19651  efgrelexlemb  19662  frgpnabllem1  19785  iscyg  19791  iscyggen  19792  gsumxp  19888  dprdval  19917  ablfac2  20003  zncyg  21485  cygznlem2a  21504  frlmsplit2  21710  evlseu  22018  tgrest  23074  ordtval  23104  ordtbas2  23106  ordtcnv  23116  ordtrest  23117  ordtrest2  23119  ispnrm  23254  cmpfi  23323  txval  23479  xkoval  23502  ptval2  23516  ptpjopn  23527  xkoccn  23534  xkoptsub  23569  xkopt  23570  fmval  23858  fmf  23860  txflf  23921  cnextf  23981  subgntr  24022  opnsubg  24023  clsnsg  24025  snclseqg  24031  tsmsval2  24045  tsmsxplem1  24068  ustuqtoplem  24154  utopsnneiplem  24162  utopsnneip  24163  fmucndlem  24205  ressprdsds  24286  mopnval  24353  metuval  24464  metdsval  24763  lebnumlem1  24887  lebnumlem3  24889  pi1xfrcnvlem  24983  pi1xfrcnv  24984  minveclem3b  25355  elovolmr  25404  ovolctb  25418  ovoliunlem3  25432  ovolshftlem1  25437  voliunlem3  25480  voliun  25482  volsup  25484  uniioombllem2  25511  uniioombllem3  25513  mbflimsup  25594  itg1climres  25642  itg2monolem1  25678  itg2i1fseq  25683  itg2cnlem1  25689  ellimc2  25805  dvivth  25942  dvne0  25943  lhop2  25947  lhop  25948  mdegfval  25994  dchrptlem2  27203  dchrpt  27205  seqsval  28218  om2noseqfo  28228  tglnunirn  28526  tgisline  28605  perpln1  28688  perpln2  28689  isperp  28690  ishpg  28737  lmif  28763  islmib  28765  edgval  29027  edgopval  29029  edgstruct  29031  uhgr2edg  29186  usgr1e  29223  cplgrop  29415  cusgrexi  29421  structtocusgr  29424  1loopgredg  29480  1egrvtxdg0  29490  umgr2v2eedg  29503  ex-ima  30422  bafval  30584  pj3i  32188  ofrn2  32622  ffsrn  32711  prodindf  32844  pfxrn2  32921  pfxrn3  32922  swrdrn2  32935  swrdrn3  32936  gsumzresunsn  33036  gsumhashmul  33041  tocycfv  33078  tocycf  33086  trsp2cyc  33092  cycpmco2f1  33093  cycpmco2rn  33094  cycpmconjvlem  33110  cycpmconjslem2  33124  qusbas2  33371  qusima  33373  qusrn  33374  nsgmgc  33377  nsgqusf1olem2  33379  idlsrgval  33468  algextdeglem4  33733  smatrcl  33809  ordtprsval  33931  ordtprsuni  33932  ordtcnvNEW  33933  ordtrestNEW  33934  ordtrest2NEW  33936  qqhval  33985  qqhval2  33995  esumval  34059  esumsnf  34077  esumrnmpt2  34081  esumfsupre  34084  esumsup  34102  sxval  34203  omsval  34306  omsfval  34307  carsggect  34331  sibf0  34347  sitgfval  34354  cvmlift3lem6  35368  satfrnmapom  35414  mvtval  35544  mvrsval  35549  mrsubvrs  35566  elmsubrn  35572  msubrn  35573  mstaval  35588  msubvrs  35604  mclsval  35607  filnetlem4  36423  mptsnunlem  37380  dissneqlem  37382  exrecfnlem  37421  ctbssinf  37448  poimirlem3  37671  poimirlem9  37677  poimirlem16  37684  poimirlem17  37685  poimirlem19  37687  poimirlem20  37688  poimirlem24  37692  poimirlem30  37698  poimirlem32  37700  mblfinlem2  37706  ovoliunnfl  37710  voliunnfl  37712  isrngo  37945  drngoi  37999  rngohomval  38012  rngoisoval  38025  idlval  38061  pridlval  38081  maxidlval  38087  igenval  38109  cnvref4  38386  symrelim  38604  unidmqs  38700  lsatset  39037  docaffvalN  41168  docafvalN  41169  aks6d1c2  42171  sticksstones2  42188  sticksstones3  42189  qsalrel  42281  prjcrvfval  42672  mzpmfp  42788  eldiophb  42798  diophrw  42800  tfsconcatrn  43383  rp-tfslim  43394  conrel1d  43704  iunrelexp0  43743  rntrclfv  43773  clsneibex  44143  neicvgbex  44153  rnsnf  45229  fsneqrn  45256  limsupval3  45738  limsupresre  45742  limsupresico  45746  limsuppnfdlem  45747  limsupvaluz  45754  limsupvaluzmpt  45763  limsupvaluz2  45784  supcnvlimsup  45786  supcnvlimsupmpt  45787  liminfval  45805  liminfval5  45811  limsupresxr  45812  liminfresxr  45813  liminfresico  45817  liminfvalxr  45829  fourierdlem60  46212  fourierdlem61  46213  sge0val  46412  sge0z  46421  sge0revalmpt  46424  sge0tsms  46426  sge0sup  46437  sge0split  46455  sge0fodjrnlem  46462  sge0seq  46492  meadjiunlem  46511  meaiuninclem  46526  omeiunle  46563  ovolval2lem  46689  ovolval4lem2  46696  ovolval5lem2  46699  ovolval5lem3  46700  ovolval5  46701  ovnovollem2  46703  smfsuplem2  46858  smfsup  46860  smfsupmpt  46861  smfinf  46864  smfinfmpt  46865  smflimsuplem1  46866  smflimsuplem2  46867  smflimsuplem4  46869  smflimsuplem5  46870  smflimsuplem7  46872  smflimsup  46874  fnrnafv  47201  afv2eq12d  47254  isubgredgss  47904  isubgredg  47905  stgredg  47995  gpgedg  48084  dmrnxp  48876  imaidfu  49150  idfudiag1lem  49563