Theorem rneqd 5926

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

Syntax hints:   → wi 4   = wceq 1567  ran crn 5660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5175  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is referenced by:  resima2  6013  elimampt  6043  imaeq1  6055  imaeq2  6056  mptimass  6073  resiima  6076  rnxpid  6169  xpima  6178  imadifssranOLD  6201  funimacnv  6615  fnima  6663  focofo  6803  rnfvprc  6873  elimampo  7545  elxp4  7915  elxp5  7916  2ndval  7985  fo2nd  8003  f2ndres  8007  curry1  8095  curry2  8098  oarec  8543  en1  9017  xpassen  9055  xpdom2  9056  sbthlem4  9074  fodomr  9112  fodomfir  9283  dffi3  9387  marypha2lem4  9394  ordtypelem9  9484  dfac12lem1  10123  dfac12r  10126  fin23lem32  10324  fin23lem34  10326  fin23lem35  10327  fin23lem36  10328  fin23lem38  10329  fin23lem39  10330  fin23lem41  10332  itunitc  10401  ttukeylem3  10491  fpwwe2lem5  10616  fpwwe2lem8  10619  wunex2  10719  wuncval2  10728  gruima  10783  rpnnen1lem6  13002  hashf1lem1  14488  s1rn  14633  s2rn  14996  s3rn  14997  s7rn  14998  relexprng  15079  relexprnd  15081  relexpfld  15082  limsupval  15521  vdwapfval  17027  vdwapval  17029  vdwmc  17034  vdwpc  17036  vdwlem6  17042  vdwlem8  17044  restval  17475  restid2  17479  prdsval  17504  prdsdsval  17527  prdsdsval2  17533  prdsdsval3  17534  imasval  17561  imasdsval  17565  isfull  17965  arwval  18096  gsumvalx  18730  conjsubg  19316  psgnfval  19566  sylow1lem2  19665  sylow1lem4  19667  sylow1  19669  sylow2blem1  19686  sylow2b  19689  sylow3lem1  19693  sylow3lem2  19694  sylow3lem3  19695  sylow3lem5  19697  sylow3lem6  19698  sylow3  19699  lsmfval  19704  lsmvalx  19705  oppglsm  19708  subglsm  19739  lsmpropd  19743  efgval2  19790  efgi2  19791  efgtlen  19792  efgsdm  19796  efgsdmi  19798  efgsrel  19800  efgs1b  19802  efgsp1  19803  efgsres  19804  efgsfo  19805  efgrelexlemb  19816  frgpnabllem1  19939  iscyg  19945  iscyggen  19946  gsumxp  20042  dprdval  20071  ablfac2  20157  zncyg  21663  cygznlem2a  21682  frlmsplit2  21888  evlseu  22199  tgrest  23281  ordtval  23311  ordtbas2  23313  ordtcnv  23323  ordtrest  23324  ordtrest2  23326  ispnrm  23461  cmpfi  23530  txval  23686  xkoval  23709  ptval2  23723  ptpjopn  23734  xkoccn  23741  xkoptsub  23776  xkopt  23777  fmval  24065  fmf  24067  txflf  24128  cnextf  24188  subgntr  24229  opnsubg  24230  clsnsg  24232  snclseqg  24238  tsmsval2  24252  tsmsxplem1  24275  ustuqtoplem  24361  utopsnneiplem  24369  utopsnneip  24370  fmucndlem  24412  ressprdsds  24493  mopnval  24560  metuval  24671  metdsval  24970  lebnumlem1  25085  lebnumlem3  25087  pi1xfrcnvlem  25180  pi1xfrcnv  25181  minveclem3b  25552  elovolmr  25600  ovolctb  25614  ovoliunlem3  25628  ovolshftlem1  25633  voliunlem3  25676  voliun  25678  volsup  25680  uniioombllem2  25707  uniioombllem3  25709  mbflimsup  25790  itg1climres  25838  itg2monolem1  25874  itg2i1fseq  25879  itg2cnlem1  25885  ellimc2  26001  dvivth  26134  dvne0  26135  lhop2  26139  lhop  26140  mdegfval  26184  dchrptlem2  27391  dchrpt  27393  seqsval  28443  om2noseqfo  28453  tglnunirn  28779  tgisline  28858  perpln1  28945  perpln2  28946  isperp  28947  ishpg  28996  tgplnfn  29011  plngval  29013  isplng  29014  lmif  29048  islmib  29050  brprlng  29139  edgval  29336  edgopval  29338  edgstruct  29340  uhgr2edg  29495  usgr1e  29532  cplgrop  29724  cusgrexi  29730  structtocusgr  29733  1loopgredg  29788  1egrvtxdg0  29798  umgr2v2eedg  29811  ex-ima  30730  bafval  30893  pj3i  32497  ofrn2  32922  rnressnsn  32959  ffsrn  33010  prodindf  33119  pfxrn2  33197  pfxrn3  33198  swrdrn2  33211  swrdrn3  33212  gsumzresunsn  33319  gsumhashmul  33324  tocycfv  33366  tocycf  33374  trsp2cyc  33380  cycpmco2f1  33381  cycpmco2rn  33382  cycpmconjvlem  33398  cycpmconjslem2  33412  domnprodeq0  33536  qusbas2  33655  qusima  33657  qusrn  33658  nsgmgc  33661  nsgqusf1olem2  33663  idlsrgval  33734  esplyfval1  33904  esplyfvaln  33905  esplyind  33906  algextdeglem4  34051  smatrcl  34127  ordtprsval  34249  ordtprsuni  34250  ordtcnvNEW  34251  ordtrestNEW  34252  ordtrest2NEW  34254  qqhval  34303  qqhval2  34313  esumval  34377  esumsnf  34395  esumrnmpt2  34399  esumfsupre  34402  esumsup  34420  sxval  34521  omsval  34624  omsfval  34625  carsggect  34649  sibf0  34665  sitgfval  34672  cvmlift3lem6  35711  satfrnmapom  35757  mvtval  35887  mvrsval  35892  mrsubvrs  35909  elmsubrn  35915  msubrn  35916  mstaval  35931  msubvrs  35947  mclsval  35950  filnetlem4  36777  mptsnunlem  37867  dissneqlem  37869  exrecfnlem  37908  ctbssinf  37935  poimirlem3  38157  poimirlem9  38163  poimirlem16  38170  poimirlem17  38171  poimirlem19  38173  poimirlem20  38174  poimirlem24  38178  poimirlem30  38184  poimirlem32  38186  mblfinlem2  38192  ovoliunnfl  38196  voliunnfl  38198  isrngo  38431  drngoi  38485  rngohomval  38498  rngoisoval  38511  idlval  38547  pridlval  38567  maxidlval  38573  igenval  38595  cnvref4  38884  symrelim  39177  unidmqs  39273  lsatset  39649  docaffvalN  41780  docafvalN  41781  aks6d1c2  42782  sticksstones2  42799  sticksstones3  42800  qsalrel  42894  prjcrvfval  43250  mzpmfp  43365  eldiophb  43375  diophrw  43377  tfsconcatrn  43956  rp-tfslim  43967  conrel1d  44276  iunrelexp0  44315  rntrclfv  44345  clsneibex  44715  neicvgbex  44725  rnsnf  45789  fsneqrn  45814  limsupval3  46293  limsupresre  46297  limsupresico  46301  limsuppnfdlem  46302  limsupvaluz  46309  limsupvaluzmpt  46318  limsupvaluz2  46339  supcnvlimsup  46341  supcnvlimsupmpt  46342  liminfval  46360  liminfval5  46366  limsupresxr  46367  liminfresxr  46368  liminfresico  46372  liminfvalxr  46384  fourierdlem60  46767  fourierdlem61  46768  sge0val  46967  sge0z  46976  sge0revalmpt  46979  sge0tsms  46981  sge0sup  46992  sge0split  47010  sge0fodjrnlem  47017  sge0seq  47047  meadjiunlem  47066  meaiuninclem  47081  omeiunle  47118  ovolval2lem  47244  ovolval4lem2  47251  ovolval5lem2  47254  ovolval5lem3  47255  ovolval5  47256  ovnovollem2  47258  smfsuplem2  47413  smfsup  47415  smfsupmpt  47416  smfinf  47419  smfinfmpt  47420  smflimsuplem1  47421  smflimsuplem2  47422  smflimsuplem4  47424  smflimsuplem5  47425  smflimsuplem7  47427  smflimsup  47429  fnrnafv  47783  afv2eq12d  47836  isubgredgss  48514  isubgredg  48515  stgredg  48605  gpgedg  48694  dmrnxp  49495  imaidfu  49768  idfudiag1lem  50181