Theorem rneqd 5274

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

Syntax hints:   → wi 4   = wceq 1475  ran crn 5039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-cnv 5046  df-dm 5048  df-rn 5049

This theorem is referenced by:  resima2  5352  resima2OLD  5353  imaeq1  5380  imaeq2  5381  resiima  5399  rnxpid  5486  xpima  5495  funimacnv  5884  fnima  5923  elxp4  7003  elxp5  7004  2ndval  7062  fo2nd  7080  f2ndres  7082  curry1  7156  curry2  7159  oarec  7529  en1  7909  xpassen  7939  xpdom2  7940  sbthlem4  7958  fodomr  7996  dffi3  8220  marypha2lem4  8227  ordtypelem9  8314  dfac12lem1  8848  dfac12r  8851  fin23lem32  9049  fin23lem34  9051  fin23lem35  9052  fin23lem36  9053  fin23lem38  9054  fin23lem39  9055  fin23lem41  9057  itunitc  9126  ttukeylem3  9216  fpwwe2lem6  9336  fpwwe2lem9  9339  wunex2  9439  wuncval2  9448  gruima  9503  rpnnen1lem6  11695  rpnnen1OLD  11701  hashf1lem1  13096  s1rn  13232  relexprng  13634  relexpfld  13637  limsupval  14053  vdwapfval  15513  vdwapval  15515  vdwmc  15520  vdwpc  15522  vdwlem6  15528  vdwlem8  15530  restval  15910  restid2  15914  prdsval  15938  prdsdsval  15961  prdsdsval2  15967  prdsdsval3  15968  imasval  15994  imasdsval  15998  isfull  16393  arwval  16516  gsumvalx  17093  conjsubg  17515  pmtrfrn  17701  psgnfval  17743  sylow1lem2  17837  sylow1lem4  17839  sylow1  17841  sylow2blem1  17858  sylow2b  17861  sylow3lem1  17865  sylow3lem2  17866  sylow3lem3  17867  sylow3lem5  17869  sylow3lem6  17870  sylow3  17871  lsmfval  17876  lsmvalx  17877  oppglsm  17880  subglsm  17909  lsmpropd  17913  efgval2  17960  efgi2  17961  efgtlen  17962  efgsdm  17966  efgsdmi  17968  efgsrel  17970  efgs1b  17972  efgsp1  17973  efgsres  17974  efgsfo  17975  efgrelexlemb  17986  frgpnabllem1  18099  iscyg  18104  iscyggen  18105  gsumxp  18198  dprdval  18225  ablfac2  18311  evlseu  19337  zncyg  19716  cygznlem2a  19735  frlmsplit2  19931  tgrest  20773  ordtval  20803  ordtbas2  20805  ordtcnv  20815  ordtrest  20816  ordtrest2  20818  ispnrm  20953  cmpfi  21021  txval  21177  xkoval  21200  ptval2  21214  ptpjopn  21225  xkoccn  21232  xkoptsub  21267  xkopt  21268  fmval  21557  fmf  21559  txflf  21620  cnextf  21680  subgntr  21720  opnsubg  21721  clsnsg  21723  snclseqg  21729  tsmsval2  21743  tsmsxplem1  21766  ustuqtoplem  21853  utopsnneiplem  21861  utopsnneip  21862  fmucndlem  21905  ressprdsds  21986  mopnval  22053  metuval  22164  metdsval  22458  lebnumlem1  22568  lebnumlem3  22570  pi1xfrcnvlem  22664  pi1xfrcnv  22665  minveclem3b  23007  elovolmr  23051  ovolctb  23065  ovoliunlem3  23079  ovolshftlem1  23084  voliunlem3  23127  voliun  23129  volsup  23131  uniioombllem2  23157  uniioombllem3  23159  mbflimsup  23239  itg1climres  23287  itg2monolem1  23323  itg2i1fseq  23328  itg2cnlem1  23334  ellimc2  23447  dvivth  23577  dvne0  23578  lhop2  23582  lhop  23583  mdegfval  23626  dchrptlem2  24790  dchrpt  24792  tglnunirn  25243  tgisline  25322  perpln1  25405  perpln2  25406  isperp  25407  ishpg  25451  lmif  25477  islmib  25479  edgaval  25794  edgaopval  25795  edgastruct  25797  edgiedgb  25798  edg0iedg0  25800  edgval  25868  edgopval  25869  edgss  25881  nbgraop  25952  nbgraopALT  25953  ex-ima  26691  bafval  26843  pj3i  28451  ofrn2  28822  ffsrn  28892  smatrcl  29190  ordtprsval  29292  ordtprsuni  29293  ordtcnvNEW  29294  ordtrestNEW  29295  ordtrest2NEW  29297  qqhval  29346  qqhval2  29354  esumval  29435  esumsnf  29453  esumrnmpt2  29457  esumfsupre  29460  esumsup  29478  sxval  29580  omsval  29682  omsfval  29683  carsggect  29707  sibf0  29723  sitgfval  29730  cvmlift3lem6  30560  mvtval  30651  mvrsval  30656  mrsubrn  30664  mrsub0  30667  mrsubf  30668  mrsubccat  30669  mrsubcn  30670  mrsubco  30672  mrsubvrs  30673  elmsubrn  30679  msubrn  30680  msubf  30683  mstaval  30695  msubvrs  30711  mclsval  30714  trpredeq1  30964  trpredeq2  30965  trpredeq3  30966  filnetlem4  31546  mptsnunlem  32361  dissneqlem  32363  poimirlem3  32582  poimirlem9  32588  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem24  32603  poimirlem30  32609  poimirlem32  32611  mblfinlem2  32617  ovoliunnfl  32621  voliunnfl  32623  isrngo  32866  drngoi  32920  rngohomval  32933  rngoisoval  32946  idlval  32982  pridlval  33002  maxidlval  33008  igenval  33030  lsatset  33295  docaffvalN  35428  docafvalN  35429  mzpmfp  36328  eldiophb  36338  diophrw  36340  conrel1d  36974  iunrelexp0  37013  rntrclfv  37043  clsneibex  37420  neicvgbex  37430  csbima12gALTOLD  38079  rnsnf  38365  fsneqrn  38398  fourierdlem60  39059  fourierdlem61  39060  sge0val  39259  sge0z  39268  sge0revalmpt  39271  sge0tsms  39273  sge0sup  39284  sge0split  39302  sge0fodjrnlem  39309  sge0seq  39339  meadjiunlem  39358  meaiuninclem  39373  omeiunle  39407  ovolval2lem  39533  ovolval4lem2  39540  ovolval5lem2  39543  ovolval5lem3  39544  ovolval5  39545  ovnovollem2  39547  fnrnafv  39891  uhgr2edg  40435  usgr1e  40471  cplgrop  40659  cusgrexi  40662  1loopgredg  40716  1egrvtxdg0  40727  umgr2v2eedg  40740