Theorem rneqd 5836

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-cnv 5588  df-dm 5590  df-rn 5591

This theorem is referenced by:  resima2  5915  imaeq1  5953  imaeq2  5954  resiima  5973  rnxpid  6065  xpima  6074  funimacnv  6499  fnima  6547  focofo  6685  rnfvprc  6750  elxp4  7743  elxp5  7744  2ndval  7807  fo2nd  7825  f2ndres  7829  curry1  7915  curry2  7918  oarec  8355  en1  8765  en1OLD  8766  xpassen  8806  xpdom2  8807  sbthlem4  8826  fodomr  8864  dffi3  9120  marypha2lem4  9127  ordtypelem9  9215  trpredeq1  9398  trpredeq2  9399  trpredeq3  9400  dfac12lem1  9830  dfac12r  9833  fin23lem32  10031  fin23lem34  10033  fin23lem35  10034  fin23lem36  10035  fin23lem38  10036  fin23lem39  10037  fin23lem41  10039  itunitc  10108  ttukeylem3  10198  fpwwe2lem5  10322  fpwwe2lem8  10325  wunex2  10425  wuncval2  10434  gruima  10489  rpnnen1lem6  12651  hashf1lem1  14096  hashf1lem1OLD  14097  s1rn  14232  relexprng  14685  relexprnd  14687  relexpfld  14688  limsupval  15111  vdwapfval  16600  vdwapval  16602  vdwmc  16607  vdwpc  16609  vdwlem6  16615  vdwlem8  16617  restval  17054  restid2  17058  prdsval  17083  prdsdsval  17106  prdsdsval2  17112  prdsdsval3  17113  imasval  17139  imasdsval  17143  isfull  17542  arwval  17674  gsumvalx  18275  conjsubg  18781  psgnfval  19023  sylow1lem2  19119  sylow1lem4  19121  sylow1  19123  sylow2blem1  19140  sylow2b  19143  sylow3lem1  19147  sylow3lem2  19148  sylow3lem3  19149  sylow3lem5  19151  sylow3lem6  19152  sylow3  19153  lsmfval  19158  lsmvalx  19159  oppglsm  19162  subglsm  19194  lsmpropd  19198  efgval2  19245  efgi2  19246  efgtlen  19247  efgsdm  19251  efgsdmi  19253  efgsrel  19255  efgs1b  19257  efgsp1  19258  efgsres  19259  efgsfo  19260  efgrelexlemb  19271  frgpnabllem1  19389  iscyg  19394  iscyggen  19395  gsumxp  19492  dprdval  19521  ablfac2  19607  rnrhmsubrg  19971  zncyg  20668  cygznlem2a  20687  frlmsplit2  20890  evlseu  21203  tgrest  22218  ordtval  22248  ordtbas2  22250  ordtcnv  22260  ordtrest  22261  ordtrest2  22263  ispnrm  22398  cmpfi  22467  txval  22623  xkoval  22646  ptval2  22660  ptpjopn  22671  xkoccn  22678  xkoptsub  22713  xkopt  22714  fmval  23002  fmf  23004  txflf  23065  cnextf  23125  subgntr  23166  opnsubg  23167  clsnsg  23169  snclseqg  23175  tsmsval2  23189  tsmsxplem1  23212  ustuqtoplem  23299  utopsnneiplem  23307  utopsnneip  23308  fmucndlem  23351  ressprdsds  23432  mopnval  23499  metuval  23611  metdsval  23916  lebnumlem1  24030  lebnumlem3  24032  pi1xfrcnvlem  24125  pi1xfrcnv  24126  minveclem3b  24497  elovolmr  24545  ovolctb  24559  ovoliunlem3  24573  ovolshftlem1  24578  voliunlem3  24621  voliun  24623  volsup  24625  uniioombllem2  24652  uniioombllem3  24654  mbflimsup  24735  itg1climres  24784  itg2monolem1  24820  itg2i1fseq  24825  itg2cnlem1  24831  ellimc2  24946  dvivth  25079  dvne0  25080  lhop2  25084  lhop  25085  mdegfval  25132  dchrptlem2  26318  dchrpt  26320  tglnunirn  26813  tgisline  26892  perpln1  26975  perpln2  26976  isperp  26977  ishpg  27024  lmif  27050  islmib  27052  edgval  27322  edgopval  27324  edgstruct  27326  uhgr2edg  27478  usgr1e  27515  cplgrop  27707  cusgrexi  27713  structtocusgr  27716  1loopgredg  27771  1egrvtxdg0  27781  umgr2v2eedg  27794  ex-ima  28707  bafval  28867  pj3i  30471  elimampt  30874  ofrn2  30878  ffsrn  30966  pfxrn2  31116  pfxrn3  31117  swrdrn2  31128  swrdrn3  31129  gsumzresunsn  31216  gsumhashmul  31218  tocycfv  31278  tocycf  31286  trsp2cyc  31292  cycpmco2f1  31293  cycpmco2rn  31294  cycpmconjvlem  31310  cycpmconjslem2  31324  qusima  31496  nsgmgc  31499  nsgqusf1olem2  31501  idlsrgval  31550  smatrcl  31648  ordtprsval  31770  ordtprsuni  31771  ordtcnvNEW  31772  ordtrestNEW  31773  ordtrest2NEW  31775  qqhval  31824  qqhval2  31832  prodindf  31891  esumval  31914  esumsnf  31932  esumrnmpt2  31936  esumfsupre  31939  esumsup  31957  sxval  32058  omsval  32160  omsfval  32161  carsggect  32185  sibf0  32201  sitgfval  32208  cvmlift3lem6  33186  satfrnmapom  33232  mvtval  33362  mvrsval  33367  mrsubvrs  33384  elmsubrn  33390  msubrn  33391  mstaval  33406  msubvrs  33422  mclsval  33425  filnetlem4  34497  mptsnunlem  35436  dissneqlem  35438  exrecfnlem  35477  ctbssinf  35504  poimirlem3  35707  poimirlem9  35713  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem24  35728  poimirlem30  35734  poimirlem32  35736  mblfinlem2  35742  ovoliunnfl  35746  voliunnfl  35748  isrngo  35982  drngoi  36036  rngohomval  36049  rngoisoval  36062  idlval  36098  pridlval  36118  maxidlval  36124  igenval  36146  symrelim  36600  unidmqs  36693  lsatset  36931  docaffvalN  39062  docafvalN  39063  sticksstones2  40031  sticksstones3  40032  qsalrel  40141  mzpmfp  40485  eldiophb  40495  diophrw  40497  conrel1d  41160  iunrelexp0  41199  rntrclfv  41229  clsneibex  41601  neicvgbex  41611  rnsnf  42610  fsneqrn  42640  mptima2  42680  limsupval3  43123  limsupresre  43127  limsupresico  43131  limsuppnfdlem  43132  limsupvaluz  43139  limsupvaluzmpt  43148  limsupvaluz2  43169  supcnvlimsup  43171  supcnvlimsupmpt  43172  liminfval  43190  liminfval5  43196  limsupresxr  43197  liminfresxr  43198  liminfresico  43202  liminfvalxr  43214  fourierdlem60  43597  fourierdlem61  43598  sge0val  43794  sge0z  43803  sge0revalmpt  43806  sge0tsms  43808  sge0sup  43819  sge0split  43837  sge0fodjrnlem  43844  sge0seq  43874  meadjiunlem  43893  meaiuninclem  43908  omeiunle  43945  ovolval2lem  44071  ovolval4lem2  44078  ovolval5lem2  44081  ovolval5lem3  44082  ovolval5  44083  ovnovollem2  44085  smfsuplem2  44232  smfsup  44234  smfsupmpt  44235  smfinf  44238  smfinfmpt  44239  smflimsuplem1  44240  smflimsuplem2  44241  smflimsuplem4  44243  smflimsuplem5  44244  smflimsuplem7  44246  smflimsup  44248  fnrnafv  44541  afv2eq12d  44594