Theorem rneqd 5850

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

Syntax hints:   → wi 4   = wceq 1539  ran crn 5591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-cnv 5598  df-dm 5600  df-rn 5601

This theorem is referenced by:  resima2  5929  imaeq1  5967  imaeq2  5968  resiima  5987  rnxpid  6081  xpima  6090  funimacnv  6522  fnima  6572  focofo  6710  rnfvprc  6777  elxp4  7778  elxp5  7779  2ndval  7843  fo2nd  7861  f2ndres  7865  curry1  7953  curry2  7956  oarec  8402  en1  8820  en1OLD  8821  xpassen  8862  xpdom2  8863  sbthlem4  8882  fodomr  8924  dffi3  9199  marypha2lem4  9206  ordtypelem9  9294  dfac12lem1  9908  dfac12r  9911  fin23lem32  10109  fin23lem34  10111  fin23lem35  10112  fin23lem36  10113  fin23lem38  10114  fin23lem39  10115  fin23lem41  10117  itunitc  10186  ttukeylem3  10276  fpwwe2lem5  10400  fpwwe2lem8  10403  wunex2  10503  wuncval2  10512  gruima  10567  rpnnen1lem6  12731  hashf1lem1  14177  hashf1lem1OLD  14178  s1rn  14313  relexprng  14766  relexprnd  14768  relexpfld  14769  limsupval  15192  vdwapfval  16681  vdwapval  16683  vdwmc  16688  vdwpc  16690  vdwlem6  16696  vdwlem8  16698  restval  17146  restid2  17150  prdsval  17175  prdsdsval  17198  prdsdsval2  17204  prdsdsval3  17205  imasval  17231  imasdsval  17235  isfull  17635  arwval  17767  gsumvalx  18369  conjsubg  18875  psgnfval  19117  sylow1lem2  19213  sylow1lem4  19215  sylow1  19217  sylow2blem1  19234  sylow2b  19237  sylow3lem1  19241  sylow3lem2  19242  sylow3lem3  19243  sylow3lem5  19245  sylow3lem6  19246  sylow3  19247  lsmfval  19252  lsmvalx  19253  oppglsm  19256  subglsm  19288  lsmpropd  19292  efgval2  19339  efgi2  19340  efgtlen  19341  efgsdm  19345  efgsdmi  19347  efgsrel  19349  efgs1b  19351  efgsp1  19352  efgsres  19353  efgsfo  19354  efgrelexlemb  19365  frgpnabllem1  19483  iscyg  19488  iscyggen  19489  gsumxp  19586  dprdval  19615  ablfac2  19701  rnrhmsubrg  20065  zncyg  20765  cygznlem2a  20784  frlmsplit2  20989  evlseu  21302  tgrest  22319  ordtval  22349  ordtbas2  22351  ordtcnv  22361  ordtrest  22362  ordtrest2  22364  ispnrm  22499  cmpfi  22568  txval  22724  xkoval  22747  ptval2  22761  ptpjopn  22772  xkoccn  22779  xkoptsub  22814  xkopt  22815  fmval  23103  fmf  23105  txflf  23166  cnextf  23226  subgntr  23267  opnsubg  23268  clsnsg  23270  snclseqg  23276  tsmsval2  23290  tsmsxplem1  23313  ustuqtoplem  23400  utopsnneiplem  23408  utopsnneip  23409  fmucndlem  23452  ressprdsds  23533  mopnval  23600  metuval  23714  metdsval  24019  lebnumlem1  24133  lebnumlem3  24135  pi1xfrcnvlem  24228  pi1xfrcnv  24229  minveclem3b  24601  elovolmr  24649  ovolctb  24663  ovoliunlem3  24677  ovolshftlem1  24682  voliunlem3  24725  voliun  24727  volsup  24729  uniioombllem2  24756  uniioombllem3  24758  mbflimsup  24839  itg1climres  24888  itg2monolem1  24924  itg2i1fseq  24929  itg2cnlem1  24935  ellimc2  25050  dvivth  25183  dvne0  25184  lhop2  25188  lhop  25189  mdegfval  25236  dchrptlem2  26422  dchrpt  26424  tglnunirn  26918  tgisline  26997  perpln1  27080  perpln2  27081  isperp  27082  ishpg  27129  lmif  27155  islmib  27157  edgval  27428  edgopval  27430  edgstruct  27432  uhgr2edg  27584  usgr1e  27621  cplgrop  27813  cusgrexi  27819  structtocusgr  27822  1loopgredg  27877  1egrvtxdg0  27887  umgr2v2eedg  27900  ex-ima  28815  bafval  28975  pj3i  30579  elimampt  30982  ofrn2  30986  ffsrn  31073  pfxrn2  31223  pfxrn3  31224  swrdrn2  31235  swrdrn3  31236  gsumzresunsn  31323  gsumhashmul  31325  tocycfv  31385  tocycf  31393  trsp2cyc  31399  cycpmco2f1  31400  cycpmco2rn  31401  cycpmconjvlem  31417  cycpmconjslem2  31431  qusima  31603  nsgmgc  31606  nsgqusf1olem2  31608  idlsrgval  31657  smatrcl  31755  ordtprsval  31877  ordtprsuni  31878  ordtcnvNEW  31879  ordtrestNEW  31880  ordtrest2NEW  31882  qqhval  31933  qqhval2  31941  prodindf  32000  esumval  32023  esumsnf  32041  esumrnmpt2  32045  esumfsupre  32048  esumsup  32066  sxval  32167  omsval  32269  omsfval  32270  carsggect  32294  sibf0  32310  sitgfval  32317  cvmlift3lem6  33295  satfrnmapom  33341  mvtval  33471  mvrsval  33476  mrsubvrs  33493  elmsubrn  33499  msubrn  33500  mstaval  33515  msubvrs  33531  mclsval  33534  filnetlem4  34579  mptsnunlem  35518  dissneqlem  35520  exrecfnlem  35559  ctbssinf  35586  poimirlem3  35789  poimirlem9  35795  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem24  35810  poimirlem30  35816  poimirlem32  35818  mblfinlem2  35824  ovoliunnfl  35828  voliunnfl  35830  isrngo  36064  drngoi  36118  rngohomval  36131  rngoisoval  36144  idlval  36180  pridlval  36200  maxidlval  36206  igenval  36228  symrelim  36680  unidmqs  36773  lsatset  37011  docaffvalN  39142  docafvalN  39143  sticksstones2  40110  sticksstones3  40111  qsalrel  40222  prjcrvfval  40475  mzpmfp  40576  eldiophb  40586  diophrw  40588  conrel1d  41278  iunrelexp0  41317  rntrclfv  41347  clsneibex  41719  neicvgbex  41729  rnsnf  42728  fsneqrn  42758  mptima2  42798  limsupval3  43240  limsupresre  43244  limsupresico  43248  limsuppnfdlem  43249  limsupvaluz  43256  limsupvaluzmpt  43265  limsupvaluz2  43286  supcnvlimsup  43288  supcnvlimsupmpt  43289  liminfval  43307  liminfval5  43313  limsupresxr  43314  liminfresxr  43315  liminfresico  43319  liminfvalxr  43331  fourierdlem60  43714  fourierdlem61  43715  sge0val  43911  sge0z  43920  sge0revalmpt  43923  sge0tsms  43925  sge0sup  43936  sge0split  43954  sge0fodjrnlem  43961  sge0seq  43991  meadjiunlem  44010  meaiuninclem  44025  omeiunle  44062  ovolval2lem  44188  ovolval4lem2  44195  ovolval5lem2  44198  ovolval5lem3  44199  ovolval5  44200  ovnovollem2  44202  smfsuplem2  44356  smfsup  44358  smfsupmpt  44359  smfinf  44362  smfinfmpt  44363  smflimsuplem1  44364  smflimsuplem2  44365  smflimsuplem4  44367  smflimsuplem5  44368  smflimsuplem7  44370  smflimsup  44372  fnrnafv  44665  afv2eq12d  44718