Theorem rneqd 5904

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

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-br 5110  df-opab 5172  df-cnv 5648  df-dm 5650  df-rn 5651

This theorem is referenced by:  resima2  5989  elimampt  6016  imaeq1  6028  imaeq2  6029  mptimass  6046  resiima  6049  imadifssran  6126  rnxpid  6148  xpima  6157  funimacnv  6599  fnima  6650  focofo  6787  rnfvprc  6854  elimampo  7528  elxp4  7900  elxp5  7901  2ndval  7973  fo2nd  7991  f2ndres  7995  curry1  8085  curry2  8088  oarec  8528  en1  8997  xpassen  9039  xpdom2  9040  sbthlem4  9059  fodomr  9097  fodomfir  9285  dffi3  9388  marypha2lem4  9395  ordtypelem9  9485  dfac12lem1  10103  dfac12r  10106  fin23lem32  10303  fin23lem34  10305  fin23lem35  10306  fin23lem36  10307  fin23lem38  10308  fin23lem39  10309  fin23lem41  10311  itunitc  10380  ttukeylem3  10470  fpwwe2lem5  10594  fpwwe2lem8  10597  wunex2  10697  wuncval2  10706  gruima  10761  rpnnen1lem6  12947  hashf1lem1  14426  s1rn  14570  s2rn  14935  s3rn  14936  s7rn  14937  relexprng  15018  relexprnd  15020  relexpfld  15021  limsupval  15446  vdwapfval  16948  vdwapval  16950  vdwmc  16955  vdwpc  16957  vdwlem6  16963  vdwlem8  16965  restval  17395  restid2  17399  prdsval  17424  prdsdsval  17447  prdsdsval2  17453  prdsdsval3  17454  imasval  17480  imasdsval  17484  isfull  17880  arwval  18011  gsumvalx  18609  conjsubg  19188  psgnfval  19436  sylow1lem2  19535  sylow1lem4  19537  sylow1  19539  sylow2blem1  19556  sylow2b  19559  sylow3lem1  19563  sylow3lem2  19564  sylow3lem3  19565  sylow3lem5  19567  sylow3lem6  19568  sylow3  19569  lsmfval  19574  lsmvalx  19575  oppglsm  19578  subglsm  19609  lsmpropd  19613  efgval2  19660  efgi2  19661  efgtlen  19662  efgsdm  19666  efgsdmi  19668  efgsrel  19670  efgs1b  19672  efgsp1  19673  efgsres  19674  efgsfo  19675  efgrelexlemb  19686  frgpnabllem1  19809  iscyg  19815  iscyggen  19816  gsumxp  19912  dprdval  19941  ablfac2  20027  zncyg  21464  cygznlem2a  21483  frlmsplit2  21688  evlseu  21996  tgrest  23052  ordtval  23082  ordtbas2  23084  ordtcnv  23094  ordtrest  23095  ordtrest2  23097  ispnrm  23232  cmpfi  23301  txval  23457  xkoval  23480  ptval2  23494  ptpjopn  23505  xkoccn  23512  xkoptsub  23547  xkopt  23548  fmval  23836  fmf  23838  txflf  23899  cnextf  23959  subgntr  24000  opnsubg  24001  clsnsg  24003  snclseqg  24009  tsmsval2  24023  tsmsxplem1  24046  ustuqtoplem  24133  utopsnneiplem  24141  utopsnneip  24142  fmucndlem  24184  ressprdsds  24265  mopnval  24332  metuval  24443  metdsval  24742  lebnumlem1  24866  lebnumlem3  24868  pi1xfrcnvlem  24962  pi1xfrcnv  24963  minveclem3b  25334  elovolmr  25383  ovolctb  25397  ovoliunlem3  25411  ovolshftlem1  25416  voliunlem3  25459  voliun  25461  volsup  25463  uniioombllem2  25490  uniioombllem3  25492  mbflimsup  25573  itg1climres  25621  itg2monolem1  25657  itg2i1fseq  25662  itg2cnlem1  25668  ellimc2  25784  dvivth  25921  dvne0  25922  lhop2  25926  lhop  25927  mdegfval  25973  dchrptlem2  27182  dchrpt  27184  seqsval  28188  om2noseqfo  28198  tglnunirn  28481  tgisline  28560  perpln1  28643  perpln2  28644  isperp  28645  ishpg  28692  lmif  28718  islmib  28720  edgval  28982  edgopval  28984  edgstruct  28986  uhgr2edg  29141  usgr1e  29178  cplgrop  29370  cusgrexi  29376  structtocusgr  29379  1loopgredg  29435  1egrvtxdg0  29445  umgr2v2eedg  29458  ex-ima  30377  bafval  30539  pj3i  32143  ofrn2  32570  ffsrn  32658  prodindf  32792  pfxrn2  32867  pfxrn3  32868  swrdrn2  32882  swrdrn3  32883  gsumzresunsn  33002  gsumhashmul  33007  tocycfv  33072  tocycf  33080  trsp2cyc  33086  cycpmco2f1  33087  cycpmco2rn  33088  cycpmconjvlem  33104  cycpmconjslem2  33118  qusbas2  33383  qusima  33385  qusrn  33386  nsgmgc  33389  nsgqusf1olem2  33391  idlsrgval  33480  algextdeglem4  33716  smatrcl  33792  ordtprsval  33914  ordtprsuni  33915  ordtcnvNEW  33916  ordtrestNEW  33917  ordtrest2NEW  33919  qqhval  33968  qqhval2  33978  esumval  34042  esumsnf  34060  esumrnmpt2  34064  esumfsupre  34067  esumsup  34085  sxval  34186  omsval  34290  omsfval  34291  carsggect  34315  sibf0  34331  sitgfval  34338  cvmlift3lem6  35311  satfrnmapom  35357  mvtval  35487  mvrsval  35492  mrsubvrs  35509  elmsubrn  35515  msubrn  35516  mstaval  35531  msubvrs  35547  mclsval  35550  filnetlem4  36364  mptsnunlem  37321  dissneqlem  37323  exrecfnlem  37362  ctbssinf  37389  poimirlem3  37612  poimirlem9  37618  poimirlem16  37625  poimirlem17  37626  poimirlem19  37628  poimirlem20  37629  poimirlem24  37633  poimirlem30  37639  poimirlem32  37641  mblfinlem2  37647  ovoliunnfl  37651  voliunnfl  37653  isrngo  37886  drngoi  37940  rngohomval  37953  rngoisoval  37966  idlval  38002  pridlval  38022  maxidlval  38028  igenval  38050  cnvref4  38327  symrelim  38545  unidmqs  38641  lsatset  38978  docaffvalN  41110  docafvalN  41111  aks6d1c2  42113  sticksstones2  42130  sticksstones3  42131  qsalrel  42223  prjcrvfval  42612  mzpmfp  42728  eldiophb  42738  diophrw  42740  tfsconcatrn  43324  rp-tfslim  43335  conrel1d  43645  iunrelexp0  43684  rntrclfv  43714  clsneibex  44084  neicvgbex  44094  rnsnf  45171  fsneqrn  45198  limsupval3  45683  limsupresre  45687  limsupresico  45691  limsuppnfdlem  45692  limsupvaluz  45699  limsupvaluzmpt  45708  limsupvaluz2  45729  supcnvlimsup  45731  supcnvlimsupmpt  45732  liminfval  45750  liminfval5  45756  limsupresxr  45757  liminfresxr  45758  liminfresico  45762  liminfvalxr  45774  fourierdlem60  46157  fourierdlem61  46158  sge0val  46357  sge0z  46366  sge0revalmpt  46369  sge0tsms  46371  sge0sup  46382  sge0split  46400  sge0fodjrnlem  46407  sge0seq  46437  meadjiunlem  46456  meaiuninclem  46471  omeiunle  46508  ovolval2lem  46634  ovolval4lem2  46641  ovolval5lem2  46644  ovolval5lem3  46645  ovolval5  46646  ovnovollem2  46648  smfsuplem2  46803  smfsup  46805  smfsupmpt  46806  smfinf  46809  smfinfmpt  46810  smflimsuplem1  46811  smflimsuplem2  46812  smflimsuplem4  46814  smflimsuplem5  46815  smflimsuplem7  46817  smflimsup  46819  fnrnafv  47153  afv2eq12d  47206  isubgredgss  47855  isubgredg  47856  stgredg  47945  gpgedg  48026  dmrnxp  48815  imaidfu  49089  idfudiag1lem  49502