Theorem rneqd 5948

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

Syntax hints:   → wi 4   = wceq 1539  ran crn 5685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143  df-opab 5205  df-cnv 5692  df-dm 5694  df-rn 5695

This theorem is referenced by:  resima2  6033  elimampt  6060  imaeq1  6072  imaeq2  6073  mptimass  6090  resiima  6093  imadifssran  6170  rnxpid  6192  xpima  6201  funimacnv  6646  fnima  6697  focofo  6832  rnfvprc  6899  elimampo  7571  elxp4  7945  elxp5  7946  2ndval  8018  fo2nd  8036  f2ndres  8040  curry1  8130  curry2  8133  oarec  8601  en1  9065  xpassen  9107  xpdom2  9108  sbthlem4  9127  fodomr  9169  fodomfir  9369  dffi3  9472  marypha2lem4  9479  ordtypelem9  9567  dfac12lem1  10185  dfac12r  10188  fin23lem32  10385  fin23lem34  10387  fin23lem35  10388  fin23lem36  10389  fin23lem38  10390  fin23lem39  10391  fin23lem41  10393  itunitc  10462  ttukeylem3  10552  fpwwe2lem5  10676  fpwwe2lem8  10679  wunex2  10779  wuncval2  10788  gruima  10843  rpnnen1lem6  13025  hashf1lem1  14495  s1rn  14638  s2rn  15003  s3rn  15004  s7rn  15005  relexprng  15086  relexprnd  15088  relexpfld  15089  limsupval  15511  vdwapfval  17010  vdwapval  17012  vdwmc  17017  vdwpc  17019  vdwlem6  17025  vdwlem8  17027  restval  17472  restid2  17476  prdsval  17501  prdsdsval  17524  prdsdsval2  17530  prdsdsval3  17531  imasval  17557  imasdsval  17561  isfull  17958  arwval  18089  gsumvalx  18690  conjsubg  19269  psgnfval  19519  sylow1lem2  19618  sylow1lem4  19620  sylow1  19622  sylow2blem1  19639  sylow2b  19642  sylow3lem1  19646  sylow3lem2  19647  sylow3lem3  19648  sylow3lem5  19650  sylow3lem6  19651  sylow3  19652  lsmfval  19657  lsmvalx  19658  oppglsm  19661  subglsm  19692  lsmpropd  19696  efgval2  19743  efgi2  19744  efgtlen  19745  efgsdm  19749  efgsdmi  19751  efgsrel  19753  efgs1b  19755  efgsp1  19756  efgsres  19757  efgsfo  19758  efgrelexlemb  19769  frgpnabllem1  19892  iscyg  19898  iscyggen  19899  gsumxp  19995  dprdval  20024  ablfac2  20110  zncyg  21568  cygznlem2a  21587  frlmsplit2  21794  evlseu  22108  tgrest  23168  ordtval  23198  ordtbas2  23200  ordtcnv  23210  ordtrest  23211  ordtrest2  23213  ispnrm  23348  cmpfi  23417  txval  23573  xkoval  23596  ptval2  23610  ptpjopn  23621  xkoccn  23628  xkoptsub  23663  xkopt  23664  fmval  23952  fmf  23954  txflf  24015  cnextf  24075  subgntr  24116  opnsubg  24117  clsnsg  24119  snclseqg  24125  tsmsval2  24139  tsmsxplem1  24162  ustuqtoplem  24249  utopsnneiplem  24257  utopsnneip  24258  fmucndlem  24301  ressprdsds  24382  mopnval  24449  metuval  24563  metdsval  24870  lebnumlem1  24994  lebnumlem3  24996  pi1xfrcnvlem  25090  pi1xfrcnv  25091  minveclem3b  25463  elovolmr  25512  ovolctb  25526  ovoliunlem3  25540  ovolshftlem1  25545  voliunlem3  25588  voliun  25590  volsup  25592  uniioombllem2  25619  uniioombllem3  25621  mbflimsup  25702  itg1climres  25750  itg2monolem1  25786  itg2i1fseq  25791  itg2cnlem1  25797  ellimc2  25913  dvivth  26050  dvne0  26051  lhop2  26055  lhop  26056  mdegfval  26102  dchrptlem2  27310  dchrpt  27312  seqsval  28295  om2noseqfo  28305  tglnunirn  28557  tgisline  28636  perpln1  28719  perpln2  28720  isperp  28721  ishpg  28768  lmif  28794  islmib  28796  edgval  29067  edgopval  29069  edgstruct  29071  uhgr2edg  29226  usgr1e  29263  cplgrop  29455  cusgrexi  29461  structtocusgr  29464  1loopgredg  29520  1egrvtxdg0  29530  umgr2v2eedg  29543  ex-ima  30462  bafval  30624  pj3i  32228  ofrn2  32651  ffsrn  32741  prodindf  32849  pfxrn2  32925  pfxrn3  32926  swrdrn2  32940  swrdrn3  32941  gsumzresunsn  33060  gsumhashmul  33065  tocycfv  33130  tocycf  33138  trsp2cyc  33144  cycpmco2f1  33145  cycpmco2rn  33146  cycpmconjvlem  33162  cycpmconjslem2  33176  qusbas2  33435  qusima  33437  qusrn  33438  nsgmgc  33441  nsgqusf1olem2  33443  idlsrgval  33532  algextdeglem4  33762  smatrcl  33796  ordtprsval  33918  ordtprsuni  33919  ordtcnvNEW  33920  ordtrestNEW  33921  ordtrest2NEW  33923  qqhval  33974  qqhval2  33984  esumval  34048  esumsnf  34066  esumrnmpt2  34070  esumfsupre  34073  esumsup  34091  sxval  34192  omsval  34296  omsfval  34297  carsggect  34321  sibf0  34337  sitgfval  34344  cvmlift3lem6  35330  satfrnmapom  35376  mvtval  35506  mvrsval  35511  mrsubvrs  35528  elmsubrn  35534  msubrn  35535  mstaval  35550  msubvrs  35566  mclsval  35569  filnetlem4  36383  mptsnunlem  37340  dissneqlem  37342  exrecfnlem  37381  ctbssinf  37408  poimirlem3  37631  poimirlem9  37637  poimirlem16  37644  poimirlem17  37645  poimirlem19  37647  poimirlem20  37648  poimirlem24  37652  poimirlem30  37658  poimirlem32  37660  mblfinlem2  37666  ovoliunnfl  37670  voliunnfl  37672  isrngo  37905  drngoi  37959  rngohomval  37972  rngoisoval  37985  idlval  38021  pridlval  38041  maxidlval  38047  igenval  38069  cnvref4  38352  symrelim  38561  unidmqs  38656  lsatset  38992  docaffvalN  41124  docafvalN  41125  aks6d1c2  42132  sticksstones2  42149  sticksstones3  42150  qsalrel  42281  prjcrvfval  42646  mzpmfp  42763  eldiophb  42773  diophrw  42775  tfsconcatrn  43360  rp-tfslim  43371  conrel1d  43681  iunrelexp0  43720  rntrclfv  43750  clsneibex  44120  neicvgbex  44130  rnsnf  45194  fsneqrn  45221  limsupval3  45712  limsupresre  45716  limsupresico  45720  limsuppnfdlem  45721  limsupvaluz  45728  limsupvaluzmpt  45737  limsupvaluz2  45758  supcnvlimsup  45760  supcnvlimsupmpt  45761  liminfval  45779  liminfval5  45785  limsupresxr  45786  liminfresxr  45787  liminfresico  45791  liminfvalxr  45803  fourierdlem60  46186  fourierdlem61  46187  sge0val  46386  sge0z  46395  sge0revalmpt  46398  sge0tsms  46400  sge0sup  46411  sge0split  46429  sge0fodjrnlem  46436  sge0seq  46466  meadjiunlem  46485  meaiuninclem  46500  omeiunle  46537  ovolval2lem  46663  ovolval4lem2  46670  ovolval5lem2  46673  ovolval5lem3  46674  ovolval5  46675  ovnovollem2  46677  smfsuplem2  46832  smfsup  46834  smfsupmpt  46835  smfinf  46838  smfinfmpt  46839  smflimsuplem1  46840  smflimsuplem2  46841  smflimsuplem4  46843  smflimsuplem5  46844  smflimsuplem7  46846  smflimsup  46848  fnrnafv  47179  afv2eq12d  47232  isubgredgss  47856  isubgredg  47857  stgredg  47928  gpgedg  48009  idfudiag1lem  49181