Theorem rneqd 5963

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

Syntax hints:   → wi 4   = wceq 1537  ran crn 5701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-cnv 5708  df-dm 5710  df-rn 5711

This theorem is referenced by:  resima2  6045  elimampt  6072  imaeq1  6084  imaeq2  6085  mptimass  6102  resiima  6105  rnxpid  6204  xpima  6213  funimacnv  6659  fnima  6710  focofo  6847  rnfvprc  6914  elimampo  7587  elxp4  7962  elxp5  7963  2ndval  8033  fo2nd  8051  f2ndres  8055  curry1  8145  curry2  8148  oarec  8618  en1  9086  en1OLD  9087  xpassen  9132  xpdom2  9133  sbthlem4  9152  fodomr  9194  fodomfir  9396  dffi3  9500  marypha2lem4  9507  ordtypelem9  9595  dfac12lem1  10213  dfac12r  10216  fin23lem32  10413  fin23lem34  10415  fin23lem35  10416  fin23lem36  10417  fin23lem38  10418  fin23lem39  10419  fin23lem41  10421  itunitc  10490  ttukeylem3  10580  fpwwe2lem5  10704  fpwwe2lem8  10707  wunex2  10807  wuncval2  10816  gruima  10871  rpnnen1lem6  13047  hashf1lem1  14504  s1rn  14647  s2rn  15012  s3rn  15013  s7rn  15014  relexprng  15095  relexprnd  15097  relexpfld  15098  limsupval  15520  vdwapfval  17018  vdwapval  17020  vdwmc  17025  vdwpc  17027  vdwlem6  17033  vdwlem8  17035  restval  17486  restid2  17490  prdsval  17515  prdsdsval  17538  prdsdsval2  17544  prdsdsval3  17545  imasval  17571  imasdsval  17575  isfull  17977  arwval  18110  gsumvalx  18714  conjsubg  19290  psgnfval  19542  sylow1lem2  19641  sylow1lem4  19643  sylow1  19645  sylow2blem1  19662  sylow2b  19665  sylow3lem1  19669  sylow3lem2  19670  sylow3lem3  19671  sylow3lem5  19673  sylow3lem6  19674  sylow3  19675  lsmfval  19680  lsmvalx  19681  oppglsm  19684  subglsm  19715  lsmpropd  19719  efgval2  19766  efgi2  19767  efgtlen  19768  efgsdm  19772  efgsdmi  19774  efgsrel  19776  efgs1b  19778  efgsp1  19779  efgsres  19780  efgsfo  19781  efgrelexlemb  19792  frgpnabllem1  19915  iscyg  19921  iscyggen  19922  gsumxp  20018  dprdval  20047  ablfac2  20133  zncyg  21590  cygznlem2a  21609  frlmsplit2  21816  evlseu  22130  tgrest  23188  ordtval  23218  ordtbas2  23220  ordtcnv  23230  ordtrest  23231  ordtrest2  23233  ispnrm  23368  cmpfi  23437  txval  23593  xkoval  23616  ptval2  23630  ptpjopn  23641  xkoccn  23648  xkoptsub  23683  xkopt  23684  fmval  23972  fmf  23974  txflf  24035  cnextf  24095  subgntr  24136  opnsubg  24137  clsnsg  24139  snclseqg  24145  tsmsval2  24159  tsmsxplem1  24182  ustuqtoplem  24269  utopsnneiplem  24277  utopsnneip  24278  fmucndlem  24321  ressprdsds  24402  mopnval  24469  metuval  24583  metdsval  24888  lebnumlem1  25012  lebnumlem3  25014  pi1xfrcnvlem  25108  pi1xfrcnv  25109  minveclem3b  25481  elovolmr  25530  ovolctb  25544  ovoliunlem3  25558  ovolshftlem1  25563  voliunlem3  25606  voliun  25608  volsup  25610  uniioombllem2  25637  uniioombllem3  25639  mbflimsup  25720  itg1climres  25769  itg2monolem1  25805  itg2i1fseq  25810  itg2cnlem1  25816  ellimc2  25932  dvivth  26069  dvne0  26070  lhop2  26074  lhop  26075  mdegfval  26121  dchrptlem2  27327  dchrpt  27329  seqsval  28312  om2noseqfo  28322  tglnunirn  28574  tgisline  28653  perpln1  28736  perpln2  28737  isperp  28738  ishpg  28785  lmif  28811  islmib  28813  edgval  29084  edgopval  29086  edgstruct  29088  uhgr2edg  29243  usgr1e  29280  cplgrop  29472  cusgrexi  29478  structtocusgr  29481  1loopgredg  29537  1egrvtxdg0  29547  umgr2v2eedg  29560  ex-ima  30474  bafval  30636  pj3i  32240  ofrn2  32659  ffsrn  32743  pfxrn2  32906  pfxrn3  32907  swrdrn2  32921  swrdrn3  32922  gsumzresunsn  33037  gsumhashmul  33040  tocycfv  33102  tocycf  33110  trsp2cyc  33116  cycpmco2f1  33117  cycpmco2rn  33118  cycpmconjvlem  33134  cycpmconjslem2  33148  qusbas2  33399  qusima  33401  qusrn  33402  nsgmgc  33405  nsgqusf1olem2  33407  idlsrgval  33496  algextdeglem4  33711  smatrcl  33742  ordtprsval  33864  ordtprsuni  33865  ordtcnvNEW  33866  ordtrestNEW  33867  ordtrest2NEW  33869  qqhval  33920  qqhval2  33928  prodindf  33987  esumval  34010  esumsnf  34028  esumrnmpt2  34032  esumfsupre  34035  esumsup  34053  sxval  34154  omsval  34258  omsfval  34259  carsggect  34283  sibf0  34299  sitgfval  34306  cvmlift3lem6  35292  satfrnmapom  35338  mvtval  35468  mvrsval  35473  mrsubvrs  35490  elmsubrn  35496  msubrn  35497  mstaval  35512  msubvrs  35528  mclsval  35531  filnetlem4  36347  mptsnunlem  37304  dissneqlem  37306  exrecfnlem  37345  ctbssinf  37372  poimirlem3  37583  poimirlem9  37589  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem24  37604  poimirlem30  37610  poimirlem32  37612  mblfinlem2  37618  ovoliunnfl  37622  voliunnfl  37624  isrngo  37857  drngoi  37911  rngohomval  37924  rngoisoval  37937  idlval  37973  pridlval  37993  maxidlval  37999  igenval  38021  cnvref4  38306  symrelim  38515  unidmqs  38610  lsatset  38946  docaffvalN  41078  docafvalN  41079  aks6d1c2  42087  sticksstones2  42104  sticksstones3  42105  qsalrel  42235  prjcrvfval  42586  mzpmfp  42703  eldiophb  42713  diophrw  42715  tfsconcatrn  43304  rp-tfslim  43315  conrel1d  43625  iunrelexp0  43664  rntrclfv  43694  clsneibex  44064  neicvgbex  44074  rnsnf  45091  fsneqrn  45118  limsupval3  45613  limsupresre  45617  limsupresico  45621  limsuppnfdlem  45622  limsupvaluz  45629  limsupvaluzmpt  45638  limsupvaluz2  45659  supcnvlimsup  45661  supcnvlimsupmpt  45662  liminfval  45680  liminfval5  45686  limsupresxr  45687  liminfresxr  45688  liminfresico  45692  liminfvalxr  45704  fourierdlem60  46087  fourierdlem61  46088  sge0val  46287  sge0z  46296  sge0revalmpt  46299  sge0tsms  46301  sge0sup  46312  sge0split  46330  sge0fodjrnlem  46337  sge0seq  46367  meadjiunlem  46386  meaiuninclem  46401  omeiunle  46438  ovolval2lem  46564  ovolval4lem2  46571  ovolval5lem2  46574  ovolval5lem3  46575  ovolval5  46576  ovnovollem2  46578  smfsuplem2  46733  smfsup  46735  smfsupmpt  46736  smfinf  46739  smfinfmpt  46740  smflimsuplem1  46741  smflimsuplem2  46742  smflimsuplem4  46744  smflimsuplem5  46745  smflimsuplem7  46747  smflimsup  46749  fnrnafv  47077  afv2eq12d  47130