Theorem rneqd 5893

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

Syntax hints:   → wi 4   = wceq 1542  ran crn 5632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  resima2  5981  elimampt  6008  imaeq1  6020  imaeq2  6021  mptimass  6038  resiima  6041  imadifssran  6115  rnxpid  6137  xpima  6146  funimacnv  6579  fnima  6628  focofo  6765  rnfvprc  6834  elimampo  7504  elxp4  7873  elxp5  7874  2ndval  7945  fo2nd  7963  f2ndres  7967  curry1  8054  curry2  8057  oarec  8497  en1  8971  xpassen  9009  xpdom2  9010  sbthlem4  9028  fodomr  9066  fodomfir  9238  dffi3  9344  marypha2lem4  9351  ordtypelem9  9441  dfac12lem1  10066  dfac12r  10069  fin23lem32  10266  fin23lem34  10268  fin23lem35  10269  fin23lem36  10270  fin23lem38  10271  fin23lem39  10272  fin23lem41  10274  itunitc  10343  ttukeylem3  10433  fpwwe2lem5  10558  fpwwe2lem8  10561  wunex2  10661  wuncval2  10670  gruima  10725  rpnnen1lem6  12932  hashf1lem1  14417  s1rn  14562  s2rn  14925  s3rn  14926  s7rn  14927  relexprng  15008  relexprnd  15010  relexpfld  15011  limsupval  15436  vdwapfval  16942  vdwapval  16944  vdwmc  16949  vdwpc  16951  vdwlem6  16957  vdwlem8  16959  restval  17389  restid2  17393  prdsval  17418  prdsdsval  17441  prdsdsval2  17447  prdsdsval3  17448  imasval  17475  imasdsval  17479  isfull  17879  arwval  18010  gsumvalx  18644  conjsubg  19225  psgnfval  19475  sylow1lem2  19574  sylow1lem4  19576  sylow1  19578  sylow2blem1  19595  sylow2b  19598  sylow3lem1  19602  sylow3lem2  19603  sylow3lem3  19604  sylow3lem5  19606  sylow3lem6  19607  sylow3  19608  lsmfval  19613  lsmvalx  19614  oppglsm  19617  subglsm  19648  lsmpropd  19652  efgval2  19699  efgi2  19700  efgtlen  19701  efgsdm  19705  efgsdmi  19707  efgsrel  19709  efgs1b  19711  efgsp1  19712  efgsres  19713  efgsfo  19714  efgrelexlemb  19725  frgpnabllem1  19848  iscyg  19854  iscyggen  19855  gsumxp  19951  dprdval  19980  ablfac2  20066  zncyg  21528  cygznlem2a  21547  frlmsplit2  21753  evlseu  22061  tgrest  23124  ordtval  23154  ordtbas2  23156  ordtcnv  23166  ordtrest  23167  ordtrest2  23169  ispnrm  23304  cmpfi  23373  txval  23529  xkoval  23552  ptval2  23566  ptpjopn  23577  xkoccn  23584  xkoptsub  23619  xkopt  23620  fmval  23908  fmf  23910  txflf  23971  cnextf  24031  subgntr  24072  opnsubg  24073  clsnsg  24075  snclseqg  24081  tsmsval2  24095  tsmsxplem1  24118  ustuqtoplem  24204  utopsnneiplem  24212  utopsnneip  24213  fmucndlem  24255  ressprdsds  24336  mopnval  24403  metuval  24514  metdsval  24813  lebnumlem1  24928  lebnumlem3  24930  pi1xfrcnvlem  25023  pi1xfrcnv  25024  minveclem3b  25395  elovolmr  25443  ovolctb  25457  ovoliunlem3  25471  ovolshftlem1  25476  voliunlem3  25519  voliun  25521  volsup  25523  uniioombllem2  25550  uniioombllem3  25552  mbflimsup  25633  itg1climres  25681  itg2monolem1  25717  itg2i1fseq  25722  itg2cnlem1  25728  ellimc2  25844  dvivth  25977  dvne0  25978  lhop2  25982  lhop  25983  mdegfval  26027  dchrptlem2  27228  dchrpt  27230  seqsval  28280  om2noseqfo  28290  tglnunirn  28616  tgisline  28695  perpln1  28778  perpln2  28779  isperp  28780  ishpg  28827  lmif  28853  islmib  28855  edgval  29118  edgopval  29120  edgstruct  29122  uhgr2edg  29277  usgr1e  29314  cplgrop  29506  cusgrexi  29512  structtocusgr  29515  1loopgredg  29570  1egrvtxdg0  29580  umgr2v2eedg  29593  ex-ima  30512  bafval  30675  pj3i  32279  ofrn2  32713  rnressnsn  32750  ffsrn  32801  prodindf  32922  pfxrn2  33000  pfxrn3  33001  swrdrn2  33014  swrdrn3  33015  gsumzresunsn  33123  gsumhashmul  33128  tocycfv  33170  tocycf  33178  trsp2cyc  33184  cycpmco2f1  33185  cycpmco2rn  33186  cycpmconjvlem  33202  cycpmconjslem2  33216  domnprodeq0  33337  qusbas2  33466  qusima  33468  qusrn  33469  nsgmgc  33472  nsgqusf1olem2  33474  idlsrgval  33563  esplyfval1  33717  esplyfvaln  33718  esplyind  33719  algextdeglem4  33864  smatrcl  33940  ordtprsval  34062  ordtprsuni  34063  ordtcnvNEW  34064  ordtrestNEW  34065  ordtrest2NEW  34067  qqhval  34116  qqhval2  34126  esumval  34190  esumsnf  34208  esumrnmpt2  34212  esumfsupre  34215  esumsup  34233  sxval  34334  omsval  34437  omsfval  34438  carsggect  34462  sibf0  34478  sitgfval  34485  cvmlift3lem6  35506  satfrnmapom  35552  mvtval  35682  mvrsval  35687  mrsubvrs  35704  elmsubrn  35710  msubrn  35711  mstaval  35726  msubvrs  35742  mclsval  35745  filnetlem4  36563  mptsnunlem  37654  dissneqlem  37656  exrecfnlem  37695  ctbssinf  37722  poimirlem3  37944  poimirlem9  37950  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem24  37965  poimirlem30  37971  poimirlem32  37973  mblfinlem2  37979  ovoliunnfl  37983  voliunnfl  37985  isrngo  38218  drngoi  38272  rngohomval  38285  rngoisoval  38298  idlval  38334  pridlval  38354  maxidlval  38360  igenval  38382  cnvref4  38671  symrelim  38964  unidmqs  39060  lsatset  39436  docaffvalN  41567  docafvalN  41568  aks6d1c2  42569  sticksstones2  42586  sticksstones3  42587  qsalrel  42680  prjcrvfval  43064  mzpmfp  43179  eldiophb  43189  diophrw  43191  tfsconcatrn  43770  rp-tfslim  43781  conrel1d  44090  iunrelexp0  44129  rntrclfv  44159  clsneibex  44529  neicvgbex  44539  rnsnf  45614  fsneqrn  45640  limsupval3  46120  limsupresre  46124  limsupresico  46128  limsuppnfdlem  46129  limsupvaluz  46136  limsupvaluzmpt  46145  limsupvaluz2  46166  supcnvlimsup  46168  supcnvlimsupmpt  46169  liminfval  46187  liminfval5  46193  limsupresxr  46194  liminfresxr  46195  liminfresico  46199  liminfvalxr  46211  fourierdlem60  46594  fourierdlem61  46595  sge0val  46794  sge0z  46803  sge0revalmpt  46806  sge0tsms  46808  sge0sup  46819  sge0split  46837  sge0fodjrnlem  46844  sge0seq  46874  meadjiunlem  46893  meaiuninclem  46908  omeiunle  46945  ovolval2lem  47071  ovolval4lem2  47078  ovolval5lem2  47081  ovolval5lem3  47082  ovolval5  47083  ovnovollem2  47085  smfsuplem2  47240  smfsup  47242  smfsupmpt  47243  smfinf  47246  smfinfmpt  47247  smflimsuplem1  47248  smflimsuplem2  47249  smflimsuplem4  47251  smflimsuplem5  47252  smflimsuplem7  47254  smflimsup  47256  fnrnafv  47610  afv2eq12d  47663  isubgredgss  48341  isubgredg  48342  stgredg  48432  gpgedg  48521  dmrnxp  49312  imaidfu  49585  idfudiag1lem  49998