Theorem rneqd 5891

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  resima2  5976  elimampt  6003  imaeq1  6015  imaeq2  6016  mptimass  6033  resiima  6036  imadifssran  6112  rnxpid  6134  xpima  6143  funimacnv  6581  fnima  6630  focofo  6767  rnfvprc  6834  elimampo  7506  elxp4  7878  elxp5  7879  2ndval  7950  fo2nd  7968  f2ndres  7972  curry1  8060  curry2  8063  oarec  8503  en1  8972  xpassen  9012  xpdom2  9013  sbthlem4  9031  fodomr  9069  fodomfir  9255  dffi3  9358  marypha2lem4  9365  ordtypelem9  9455  dfac12lem1  10073  dfac12r  10076  fin23lem32  10273  fin23lem34  10275  fin23lem35  10276  fin23lem36  10277  fin23lem38  10278  fin23lem39  10279  fin23lem41  10281  itunitc  10350  ttukeylem3  10440  fpwwe2lem5  10564  fpwwe2lem8  10567  wunex2  10667  wuncval2  10676  gruima  10731  rpnnen1lem6  12917  hashf1lem1  14396  s1rn  14540  s2rn  14905  s3rn  14906  s7rn  14907  relexprng  14988  relexprnd  14990  relexpfld  14991  limsupval  15416  vdwapfval  16918  vdwapval  16920  vdwmc  16925  vdwpc  16927  vdwlem6  16933  vdwlem8  16935  restval  17365  restid2  17369  prdsval  17394  prdsdsval  17417  prdsdsval2  17423  prdsdsval3  17424  imasval  17450  imasdsval  17454  isfull  17850  arwval  17981  gsumvalx  18579  conjsubg  19158  psgnfval  19406  sylow1lem2  19505  sylow1lem4  19507  sylow1  19509  sylow2blem1  19526  sylow2b  19529  sylow3lem1  19533  sylow3lem2  19534  sylow3lem3  19535  sylow3lem5  19537  sylow3lem6  19538  sylow3  19539  lsmfval  19544  lsmvalx  19545  oppglsm  19548  subglsm  19579  lsmpropd  19583  efgval2  19630  efgi2  19631  efgtlen  19632  efgsdm  19636  efgsdmi  19638  efgsrel  19640  efgs1b  19642  efgsp1  19643  efgsres  19644  efgsfo  19645  efgrelexlemb  19656  frgpnabllem1  19779  iscyg  19785  iscyggen  19786  gsumxp  19882  dprdval  19911  ablfac2  19997  zncyg  21434  cygznlem2a  21453  frlmsplit2  21658  evlseu  21966  tgrest  23022  ordtval  23052  ordtbas2  23054  ordtcnv  23064  ordtrest  23065  ordtrest2  23067  ispnrm  23202  cmpfi  23271  txval  23427  xkoval  23450  ptval2  23464  ptpjopn  23475  xkoccn  23482  xkoptsub  23517  xkopt  23518  fmval  23806  fmf  23808  txflf  23869  cnextf  23929  subgntr  23970  opnsubg  23971  clsnsg  23973  snclseqg  23979  tsmsval2  23993  tsmsxplem1  24016  ustuqtoplem  24103  utopsnneiplem  24111  utopsnneip  24112  fmucndlem  24154  ressprdsds  24235  mopnval  24302  metuval  24413  metdsval  24712  lebnumlem1  24836  lebnumlem3  24838  pi1xfrcnvlem  24932  pi1xfrcnv  24933  minveclem3b  25304  elovolmr  25353  ovolctb  25367  ovoliunlem3  25381  ovolshftlem1  25386  voliunlem3  25429  voliun  25431  volsup  25433  uniioombllem2  25460  uniioombllem3  25462  mbflimsup  25543  itg1climres  25591  itg2monolem1  25627  itg2i1fseq  25632  itg2cnlem1  25638  ellimc2  25754  dvivth  25891  dvne0  25892  lhop2  25896  lhop  25897  mdegfval  25943  dchrptlem2  27152  dchrpt  27154  seqsval  28158  om2noseqfo  28168  tglnunirn  28451  tgisline  28530  perpln1  28613  perpln2  28614  isperp  28615  ishpg  28662  lmif  28688  islmib  28690  edgval  28952  edgopval  28954  edgstruct  28956  uhgr2edg  29111  usgr1e  29148  cplgrop  29340  cusgrexi  29346  structtocusgr  29349  1loopgredg  29405  1egrvtxdg0  29415  umgr2v2eedg  29428  ex-ima  30344  bafval  30506  pj3i  32110  ofrn2  32537  ffsrn  32625  prodindf  32759  pfxrn2  32834  pfxrn3  32835  swrdrn2  32849  swrdrn3  32850  gsumzresunsn  32969  gsumhashmul  32974  tocycfv  33039  tocycf  33047  trsp2cyc  33053  cycpmco2f1  33054  cycpmco2rn  33055  cycpmconjvlem  33071  cycpmconjslem2  33085  qusbas2  33350  qusima  33352  qusrn  33353  nsgmgc  33356  nsgqusf1olem2  33358  idlsrgval  33447  algextdeglem4  33683  smatrcl  33759  ordtprsval  33881  ordtprsuni  33882  ordtcnvNEW  33883  ordtrestNEW  33884  ordtrest2NEW  33886  qqhval  33935  qqhval2  33945  esumval  34009  esumsnf  34027  esumrnmpt2  34031  esumfsupre  34034  esumsup  34052  sxval  34153  omsval  34257  omsfval  34258  carsggect  34282  sibf0  34298  sitgfval  34305  cvmlift3lem6  35284  satfrnmapom  35330  mvtval  35460  mvrsval  35465  mrsubvrs  35482  elmsubrn  35488  msubrn  35489  mstaval  35504  msubvrs  35520  mclsval  35523  filnetlem4  36342  mptsnunlem  37299  dissneqlem  37301  exrecfnlem  37340  ctbssinf  37367  poimirlem3  37590  poimirlem9  37596  poimirlem16  37603  poimirlem17  37604  poimirlem19  37606  poimirlem20  37607  poimirlem24  37611  poimirlem30  37617  poimirlem32  37619  mblfinlem2  37625  ovoliunnfl  37629  voliunnfl  37631  isrngo  37864  drngoi  37918  rngohomval  37931  rngoisoval  37944  idlval  37980  pridlval  38000  maxidlval  38006  igenval  38028  cnvref4  38305  symrelim  38523  unidmqs  38619  lsatset  38956  docaffvalN  41088  docafvalN  41089  aks6d1c2  42091  sticksstones2  42108  sticksstones3  42109  qsalrel  42201  prjcrvfval  42592  mzpmfp  42708  eldiophb  42718  diophrw  42720  tfsconcatrn  43304  rp-tfslim  43315  conrel1d  43625  iunrelexp0  43664  rntrclfv  43694  clsneibex  44064  neicvgbex  44074  rnsnf  45151  fsneqrn  45178  limsupval3  45663  limsupresre  45667  limsupresico  45671  limsuppnfdlem  45672  limsupvaluz  45679  limsupvaluzmpt  45688  limsupvaluz2  45709  supcnvlimsup  45711  supcnvlimsupmpt  45712  liminfval  45730  liminfval5  45736  limsupresxr  45737  liminfresxr  45738  liminfresico  45742  liminfvalxr  45754  fourierdlem60  46137  fourierdlem61  46138  sge0val  46337  sge0z  46346  sge0revalmpt  46349  sge0tsms  46351  sge0sup  46362  sge0split  46380  sge0fodjrnlem  46387  sge0seq  46417  meadjiunlem  46436  meaiuninclem  46451  omeiunle  46488  ovolval2lem  46614  ovolval4lem2  46621  ovolval5lem2  46624  ovolval5lem3  46625  ovolval5  46626  ovnovollem2  46628  smfsuplem2  46783  smfsup  46785  smfsupmpt  46786  smfinf  46789  smfinfmpt  46790  smflimsuplem1  46791  smflimsuplem2  46792  smflimsuplem4  46794  smflimsuplem5  46795  smflimsuplem7  46797  smflimsup  46799  fnrnafv  47136  afv2eq12d  47189  isubgredgss  47838  isubgredg  47839  stgredg  47928  gpgedg  48009  dmrnxp  48798  imaidfu  49072  idfudiag1lem  49485