Theorem rneqd 5887

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

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

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  resima2  5975  elimampt  6002  imaeq1  6014  imaeq2  6015  mptimass  6032  resiima  6035  imadifssran  6109  rnxpid  6131  xpima  6140  funimacnv  6573  fnima  6622  focofo  6759  rnfvprc  6828  elimampo  7495  elxp4  7864  elxp5  7865  2ndval  7936  fo2nd  7954  f2ndres  7958  curry1  8046  curry2  8049  oarec  8489  en1  8961  xpassen  8999  xpdom2  9000  sbthlem4  9018  fodomr  9056  fodomfir  9228  dffi3  9334  marypha2lem4  9341  ordtypelem9  9431  dfac12lem1  10054  dfac12r  10057  fin23lem32  10254  fin23lem34  10256  fin23lem35  10257  fin23lem36  10258  fin23lem38  10259  fin23lem39  10260  fin23lem41  10262  itunitc  10331  ttukeylem3  10421  fpwwe2lem5  10546  fpwwe2lem8  10549  wunex2  10649  wuncval2  10658  gruima  10713  rpnnen1lem6  12895  hashf1lem1  14378  s1rn  14523  s2rn  14886  s3rn  14887  s7rn  14888  relexprng  14969  relexprnd  14971  relexpfld  14972  limsupval  15397  vdwapfval  16899  vdwapval  16901  vdwmc  16906  vdwpc  16908  vdwlem6  16914  vdwlem8  16916  restval  17346  restid2  17350  prdsval  17375  prdsdsval  17398  prdsdsval2  17404  prdsdsval3  17405  imasval  17432  imasdsval  17436  isfull  17836  arwval  17967  gsumvalx  18601  conjsubg  19179  psgnfval  19429  sylow1lem2  19528  sylow1lem4  19530  sylow1  19532  sylow2blem1  19549  sylow2b  19552  sylow3lem1  19556  sylow3lem2  19557  sylow3lem3  19558  sylow3lem5  19560  sylow3lem6  19561  sylow3  19562  lsmfval  19567  lsmvalx  19568  oppglsm  19571  subglsm  19602  lsmpropd  19606  efgval2  19653  efgi2  19654  efgtlen  19655  efgsdm  19659  efgsdmi  19661  efgsrel  19663  efgs1b  19665  efgsp1  19666  efgsres  19667  efgsfo  19668  efgrelexlemb  19679  frgpnabllem1  19802  iscyg  19808  iscyggen  19809  gsumxp  19905  dprdval  19934  ablfac2  20020  zncyg  21503  cygznlem2a  21522  frlmsplit2  21728  evlseu  22038  tgrest  23103  ordtval  23133  ordtbas2  23135  ordtcnv  23145  ordtrest  23146  ordtrest2  23148  ispnrm  23283  cmpfi  23352  txval  23508  xkoval  23531  ptval2  23545  ptpjopn  23556  xkoccn  23563  xkoptsub  23598  xkopt  23599  fmval  23887  fmf  23889  txflf  23950  cnextf  24010  subgntr  24051  opnsubg  24052  clsnsg  24054  snclseqg  24060  tsmsval2  24074  tsmsxplem1  24097  ustuqtoplem  24183  utopsnneiplem  24191  utopsnneip  24192  fmucndlem  24234  ressprdsds  24315  mopnval  24382  metuval  24493  metdsval  24792  lebnumlem1  24916  lebnumlem3  24918  pi1xfrcnvlem  25012  pi1xfrcnv  25013  minveclem3b  25384  elovolmr  25433  ovolctb  25447  ovoliunlem3  25461  ovolshftlem1  25466  voliunlem3  25509  voliun  25511  volsup  25513  uniioombllem2  25540  uniioombllem3  25542  mbflimsup  25623  itg1climres  25671  itg2monolem1  25707  itg2i1fseq  25712  itg2cnlem1  25718  ellimc2  25834  dvivth  25971  dvne0  25972  lhop2  25976  lhop  25977  mdegfval  26023  dchrptlem2  27232  dchrpt  27234  seqsval  28284  om2noseqfo  28294  tglnunirn  28620  tgisline  28699  perpln1  28782  perpln2  28783  isperp  28784  ishpg  28831  lmif  28857  islmib  28859  edgval  29122  edgopval  29124  edgstruct  29126  uhgr2edg  29281  usgr1e  29318  cplgrop  29510  cusgrexi  29516  structtocusgr  29519  1loopgredg  29575  1egrvtxdg0  29585  umgr2v2eedg  29598  ex-ima  30517  bafval  30679  pj3i  32283  ofrn2  32718  rnressnsn  32756  ffsrn  32807  prodindf  32944  pfxrn2  33022  pfxrn3  33023  swrdrn2  33036  swrdrn3  33037  gsumzresunsn  33145  gsumhashmul  33150  tocycfv  33191  tocycf  33199  trsp2cyc  33205  cycpmco2f1  33206  cycpmco2rn  33207  cycpmconjvlem  33223  cycpmconjslem2  33237  domnprodeq0  33358  qusbas2  33487  qusima  33489  qusrn  33490  nsgmgc  33493  nsgqusf1olem2  33495  idlsrgval  33584  esplyind  33731  algextdeglem4  33877  smatrcl  33953  ordtprsval  34075  ordtprsuni  34076  ordtcnvNEW  34077  ordtrestNEW  34078  ordtrest2NEW  34080  qqhval  34129  qqhval2  34139  esumval  34203  esumsnf  34221  esumrnmpt2  34225  esumfsupre  34228  esumsup  34246  sxval  34347  omsval  34450  omsfval  34451  carsggect  34475  sibf0  34491  sitgfval  34498  cvmlift3lem6  35518  satfrnmapom  35564  mvtval  35694  mvrsval  35699  mrsubvrs  35716  elmsubrn  35722  msubrn  35723  mstaval  35738  msubvrs  35754  mclsval  35757  filnetlem4  36575  mptsnunlem  37543  dissneqlem  37545  exrecfnlem  37584  ctbssinf  37611  poimirlem3  37824  poimirlem9  37830  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem24  37845  poimirlem30  37851  poimirlem32  37853  mblfinlem2  37859  ovoliunnfl  37863  voliunnfl  37865  isrngo  38098  drngoi  38152  rngohomval  38165  rngoisoval  38178  idlval  38214  pridlval  38234  maxidlval  38240  igenval  38262  cnvref4  38543  symrelim  38816  unidmqs  38913  lsatset  39250  docaffvalN  41381  docafvalN  41382  aks6d1c2  42384  sticksstones2  42401  sticksstones3  42402  qsalrel  42496  prjcrvfval  42874  mzpmfp  42989  eldiophb  42999  diophrw  43001  tfsconcatrn  43584  rp-tfslim  43595  conrel1d  43904  iunrelexp0  43943  rntrclfv  43973  clsneibex  44343  neicvgbex  44353  rnsnf  45428  fsneqrn  45455  limsupval3  45936  limsupresre  45940  limsupresico  45944  limsuppnfdlem  45945  limsupvaluz  45952  limsupvaluzmpt  45961  limsupvaluz2  45982  supcnvlimsup  45984  supcnvlimsupmpt  45985  liminfval  46003  liminfval5  46009  limsupresxr  46010  liminfresxr  46011  liminfresico  46015  liminfvalxr  46027  fourierdlem60  46410  fourierdlem61  46411  sge0val  46610  sge0z  46619  sge0revalmpt  46622  sge0tsms  46624  sge0sup  46635  sge0split  46653  sge0fodjrnlem  46660  sge0seq  46690  meadjiunlem  46709  meaiuninclem  46724  omeiunle  46761  ovolval2lem  46887  ovolval4lem2  46894  ovolval5lem2  46897  ovolval5lem3  46898  ovolval5  46899  ovnovollem2  46901  smfsuplem2  47056  smfsup  47058  smfsupmpt  47059  smfinf  47062  smfinfmpt  47063  smflimsuplem1  47064  smflimsuplem2  47065  smflimsuplem4  47067  smflimsuplem5  47068  smflimsuplem7  47070  smflimsup  47072  fnrnafv  47408  afv2eq12d  47461  isubgredgss  48111  isubgredg  48112  stgredg  48202  gpgedg  48291  dmrnxp  49082  imaidfu  49355  idfudiag1lem  49768