Theorem rneqd 5951

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

Syntax hints:   → wi 4   = wceq 1536  ran crn 5689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-cnv 5696  df-dm 5698  df-rn 5699

This theorem is referenced by:  resima2  6035  elimampt  6062  imaeq1  6074  imaeq2  6075  mptimass  6092  resiima  6095  rnxpid  6194  xpima  6203  funimacnv  6648  fnima  6698  focofo  6833  rnfvprc  6900  elimampo  7569  elxp4  7944  elxp5  7945  2ndval  8015  fo2nd  8033  f2ndres  8037  curry1  8127  curry2  8130  oarec  8598  en1  9062  xpassen  9104  xpdom2  9105  sbthlem4  9124  fodomr  9166  fodomfir  9365  dffi3  9468  marypha2lem4  9475  ordtypelem9  9563  dfac12lem1  10181  dfac12r  10184  fin23lem32  10381  fin23lem34  10383  fin23lem35  10384  fin23lem36  10385  fin23lem38  10386  fin23lem39  10387  fin23lem41  10389  itunitc  10458  ttukeylem3  10548  fpwwe2lem5  10672  fpwwe2lem8  10675  wunex2  10775  wuncval2  10784  gruima  10839  rpnnen1lem6  13021  hashf1lem1  14490  s1rn  14633  s2rn  14998  s3rn  14999  s7rn  15000  relexprng  15081  relexprnd  15083  relexpfld  15084  limsupval  15506  vdwapfval  17004  vdwapval  17006  vdwmc  17011  vdwpc  17013  vdwlem6  17019  vdwlem8  17021  restval  17472  restid2  17476  prdsval  17501  prdsdsval  17524  prdsdsval2  17530  prdsdsval3  17531  imasval  17557  imasdsval  17561  isfull  17963  arwval  18096  gsumvalx  18701  conjsubg  19280  psgnfval  19532  sylow1lem2  19631  sylow1lem4  19633  sylow1  19635  sylow2blem1  19652  sylow2b  19655  sylow3lem1  19659  sylow3lem2  19660  sylow3lem3  19661  sylow3lem5  19663  sylow3lem6  19664  sylow3  19665  lsmfval  19670  lsmvalx  19671  oppglsm  19674  subglsm  19705  lsmpropd  19709  efgval2  19756  efgi2  19757  efgtlen  19758  efgsdm  19762  efgsdmi  19764  efgsrel  19766  efgs1b  19768  efgsp1  19769  efgsres  19770  efgsfo  19771  efgrelexlemb  19782  frgpnabllem1  19905  iscyg  19911  iscyggen  19912  gsumxp  20008  dprdval  20037  ablfac2  20123  zncyg  21584  cygznlem2a  21603  frlmsplit2  21810  evlseu  22124  tgrest  23182  ordtval  23212  ordtbas2  23214  ordtcnv  23224  ordtrest  23225  ordtrest2  23227  ispnrm  23362  cmpfi  23431  txval  23587  xkoval  23610  ptval2  23624  ptpjopn  23635  xkoccn  23642  xkoptsub  23677  xkopt  23678  fmval  23966  fmf  23968  txflf  24029  cnextf  24089  subgntr  24130  opnsubg  24131  clsnsg  24133  snclseqg  24139  tsmsval2  24153  tsmsxplem1  24176  ustuqtoplem  24263  utopsnneiplem  24271  utopsnneip  24272  fmucndlem  24315  ressprdsds  24396  mopnval  24463  metuval  24577  metdsval  24882  lebnumlem1  25006  lebnumlem3  25008  pi1xfrcnvlem  25102  pi1xfrcnv  25103  minveclem3b  25475  elovolmr  25524  ovolctb  25538  ovoliunlem3  25552  ovolshftlem1  25557  voliunlem3  25600  voliun  25602  volsup  25604  uniioombllem2  25631  uniioombllem3  25633  mbflimsup  25714  itg1climres  25763  itg2monolem1  25799  itg2i1fseq  25804  itg2cnlem1  25810  ellimc2  25926  dvivth  26063  dvne0  26064  lhop2  26068  lhop  26069  mdegfval  26115  dchrptlem2  27323  dchrpt  27325  seqsval  28308  om2noseqfo  28318  tglnunirn  28570  tgisline  28649  perpln1  28732  perpln2  28733  isperp  28734  ishpg  28781  lmif  28807  islmib  28809  edgval  29080  edgopval  29082  edgstruct  29084  uhgr2edg  29239  usgr1e  29276  cplgrop  29468  cusgrexi  29474  structtocusgr  29477  1loopgredg  29533  1egrvtxdg0  29543  umgr2v2eedg  29556  ex-ima  30470  bafval  30632  pj3i  32236  ofrn2  32656  ffsrn  32746  pfxrn2  32908  pfxrn3  32909  swrdrn2  32923  swrdrn3  32924  gsumzresunsn  33041  gsumhashmul  33046  tocycfv  33111  tocycf  33119  trsp2cyc  33125  cycpmco2f1  33126  cycpmco2rn  33127  cycpmconjvlem  33143  cycpmconjslem2  33157  qusbas2  33413  qusima  33415  qusrn  33416  nsgmgc  33419  nsgqusf1olem2  33421  idlsrgval  33510  algextdeglem4  33725  smatrcl  33756  ordtprsval  33878  ordtprsuni  33879  ordtcnvNEW  33880  ordtrestNEW  33881  ordtrest2NEW  33883  qqhval  33934  qqhval2  33944  prodindf  34003  esumval  34026  esumsnf  34044  esumrnmpt2  34048  esumfsupre  34051  esumsup  34069  sxval  34170  omsval  34274  omsfval  34275  carsggect  34299  sibf0  34315  sitgfval  34322  cvmlift3lem6  35308  satfrnmapom  35354  mvtval  35484  mvrsval  35489  mrsubvrs  35506  elmsubrn  35512  msubrn  35513  mstaval  35528  msubvrs  35544  mclsval  35547  filnetlem4  36363  mptsnunlem  37320  dissneqlem  37322  exrecfnlem  37361  ctbssinf  37388  poimirlem3  37609  poimirlem9  37615  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem24  37630  poimirlem30  37636  poimirlem32  37638  mblfinlem2  37644  ovoliunnfl  37648  voliunnfl  37650  isrngo  37883  drngoi  37937  rngohomval  37950  rngoisoval  37963  idlval  37999  pridlval  38019  maxidlval  38025  igenval  38047  cnvref4  38331  symrelim  38540  unidmqs  38635  lsatset  38971  docaffvalN  41103  docafvalN  41104  aks6d1c2  42111  sticksstones2  42128  sticksstones3  42129  qsalrel  42259  prjcrvfval  42617  mzpmfp  42734  eldiophb  42744  diophrw  42746  tfsconcatrn  43331  rp-tfslim  43342  conrel1d  43652  iunrelexp0  43691  rntrclfv  43721  clsneibex  44091  neicvgbex  44101  rnsnf  45126  fsneqrn  45153  limsupval3  45647  limsupresre  45651  limsupresico  45655  limsuppnfdlem  45656  limsupvaluz  45663  limsupvaluzmpt  45672  limsupvaluz2  45693  supcnvlimsup  45695  supcnvlimsupmpt  45696  liminfval  45714  liminfval5  45720  limsupresxr  45721  liminfresxr  45722  liminfresico  45726  liminfvalxr  45738  fourierdlem60  46121  fourierdlem61  46122  sge0val  46321  sge0z  46330  sge0revalmpt  46333  sge0tsms  46335  sge0sup  46346  sge0split  46364  sge0fodjrnlem  46371  sge0seq  46401  meadjiunlem  46420  meaiuninclem  46435  omeiunle  46472  ovolval2lem  46598  ovolval4lem2  46605  ovolval5lem2  46608  ovolval5lem3  46609  ovolval5  46610  ovnovollem2  46612  smfsuplem2  46767  smfsup  46769  smfsupmpt  46770  smfinf  46773  smfinfmpt  46774  smflimsuplem1  46775  smflimsuplem2  46776  smflimsuplem4  46778  smflimsuplem5  46779  smflimsuplem7  46781  smflimsup  46783  fnrnafv  47111  afv2eq12d  47164  isubgredgss  47788  isubgredg  47789  stgredg  47858  gpgedg  47939