Theorem rneqd 5846

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-br 5080  df-opab 5142  df-cnv 5598  df-dm 5600  df-rn 5601

This theorem is referenced by:  resima2  5925  imaeq1  5963  imaeq2  5964  resiima  5983  rnxpid  6075  xpima  6084  funimacnv  6513  fnima  6561  focofo  6699  rnfvprc  6765  elxp4  7763  elxp5  7764  2ndval  7827  fo2nd  7845  f2ndres  7849  curry1  7935  curry2  7938  oarec  8378  en1  8794  en1OLD  8795  xpassen  8835  xpdom2  8836  sbthlem4  8855  fodomr  8897  dffi3  9168  marypha2lem4  9175  ordtypelem9  9263  trpredeq1  9467  trpredeq2  9468  trpredeq3  9469  dfac12lem1  9900  dfac12r  9903  fin23lem32  10101  fin23lem34  10103  fin23lem35  10104  fin23lem36  10105  fin23lem38  10106  fin23lem39  10107  fin23lem41  10109  itunitc  10178  ttukeylem3  10268  fpwwe2lem5  10392  fpwwe2lem8  10395  wunex2  10495  wuncval2  10504  gruima  10559  rpnnen1lem6  12721  hashf1lem1  14166  hashf1lem1OLD  14167  s1rn  14302  relexprng  14755  relexprnd  14757  relexpfld  14758  limsupval  15181  vdwapfval  16670  vdwapval  16672  vdwmc  16677  vdwpc  16679  vdwlem6  16685  vdwlem8  16687  restval  17135  restid2  17139  prdsval  17164  prdsdsval  17187  prdsdsval2  17193  prdsdsval3  17194  imasval  17220  imasdsval  17224  isfull  17624  arwval  17756  gsumvalx  18358  conjsubg  18864  psgnfval  19106  sylow1lem2  19202  sylow1lem4  19204  sylow1  19206  sylow2blem1  19223  sylow2b  19226  sylow3lem1  19230  sylow3lem2  19231  sylow3lem3  19232  sylow3lem5  19234  sylow3lem6  19235  sylow3  19236  lsmfval  19241  lsmvalx  19242  oppglsm  19245  subglsm  19277  lsmpropd  19281  efgval2  19328  efgi2  19329  efgtlen  19330  efgsdm  19334  efgsdmi  19336  efgsrel  19338  efgs1b  19340  efgsp1  19341  efgsres  19342  efgsfo  19343  efgrelexlemb  19354  frgpnabllem1  19472  iscyg  19477  iscyggen  19478  gsumxp  19575  dprdval  19604  ablfac2  19690  rnrhmsubrg  20054  zncyg  20754  cygznlem2a  20773  frlmsplit2  20978  evlseu  21291  tgrest  22308  ordtval  22338  ordtbas2  22340  ordtcnv  22350  ordtrest  22351  ordtrest2  22353  ispnrm  22488  cmpfi  22557  txval  22713  xkoval  22736  ptval2  22750  ptpjopn  22761  xkoccn  22768  xkoptsub  22803  xkopt  22804  fmval  23092  fmf  23094  txflf  23155  cnextf  23215  subgntr  23256  opnsubg  23257  clsnsg  23259  snclseqg  23265  tsmsval2  23279  tsmsxplem1  23302  ustuqtoplem  23389  utopsnneiplem  23397  utopsnneip  23398  fmucndlem  23441  ressprdsds  23522  mopnval  23589  metuval  23703  metdsval  24008  lebnumlem1  24122  lebnumlem3  24124  pi1xfrcnvlem  24217  pi1xfrcnv  24218  minveclem3b  24590  elovolmr  24638  ovolctb  24652  ovoliunlem3  24666  ovolshftlem1  24671  voliunlem3  24714  voliun  24716  volsup  24718  uniioombllem2  24745  uniioombllem3  24747  mbflimsup  24828  itg1climres  24877  itg2monolem1  24913  itg2i1fseq  24918  itg2cnlem1  24924  ellimc2  25039  dvivth  25172  dvne0  25173  lhop2  25177  lhop  25178  mdegfval  25225  dchrptlem2  26411  dchrpt  26413  tglnunirn  26907  tgisline  26986  perpln1  27069  perpln2  27070  isperp  27071  ishpg  27118  lmif  27144  islmib  27146  edgval  27417  edgopval  27419  edgstruct  27421  uhgr2edg  27573  usgr1e  27610  cplgrop  27802  cusgrexi  27808  structtocusgr  27811  1loopgredg  27866  1egrvtxdg0  27876  umgr2v2eedg  27889  ex-ima  28802  bafval  28962  pj3i  30566  elimampt  30969  ofrn2  30973  ffsrn  31060  pfxrn2  31210  pfxrn3  31211  swrdrn2  31222  swrdrn3  31223  gsumzresunsn  31310  gsumhashmul  31312  tocycfv  31372  tocycf  31380  trsp2cyc  31386  cycpmco2f1  31387  cycpmco2rn  31388  cycpmconjvlem  31404  cycpmconjslem2  31418  qusima  31590  nsgmgc  31593  nsgqusf1olem2  31595  idlsrgval  31644  smatrcl  31742  ordtprsval  31864  ordtprsuni  31865  ordtcnvNEW  31866  ordtrestNEW  31867  ordtrest2NEW  31869  qqhval  31920  qqhval2  31928  prodindf  31987  esumval  32010  esumsnf  32028  esumrnmpt2  32032  esumfsupre  32035  esumsup  32053  sxval  32154  omsval  32256  omsfval  32257  carsggect  32281  sibf0  32297  sitgfval  32304  cvmlift3lem6  33282  satfrnmapom  33328  mvtval  33458  mvrsval  33463  mrsubvrs  33480  elmsubrn  33486  msubrn  33487  mstaval  33502  msubvrs  33518  mclsval  33521  filnetlem4  34566  mptsnunlem  35505  dissneqlem  35507  exrecfnlem  35546  ctbssinf  35573  poimirlem3  35776  poimirlem9  35782  poimirlem16  35789  poimirlem17  35790  poimirlem19  35792  poimirlem20  35793  poimirlem24  35797  poimirlem30  35803  poimirlem32  35805  mblfinlem2  35811  ovoliunnfl  35815  voliunnfl  35817  isrngo  36051  drngoi  36105  rngohomval  36118  rngoisoval  36131  idlval  36167  pridlval  36187  maxidlval  36193  igenval  36215  symrelim  36669  unidmqs  36762  lsatset  37000  docaffvalN  39131  docafvalN  39132  sticksstones2  40100  sticksstones3  40101  qsalrel  40212  prjcrvfval  40465  mzpmfp  40566  eldiophb  40576  diophrw  40578  conrel1d  41241  iunrelexp0  41280  rntrclfv  41310  clsneibex  41682  neicvgbex  41692  rnsnf  42691  fsneqrn  42721  mptima2  42761  limsupval3  43204  limsupresre  43208  limsupresico  43212  limsuppnfdlem  43213  limsupvaluz  43220  limsupvaluzmpt  43229  limsupvaluz2  43250  supcnvlimsup  43252  supcnvlimsupmpt  43253  liminfval  43271  liminfval5  43277  limsupresxr  43278  liminfresxr  43279  liminfresico  43283  liminfvalxr  43295  fourierdlem60  43678  fourierdlem61  43679  sge0val  43875  sge0z  43884  sge0revalmpt  43887  sge0tsms  43889  sge0sup  43900  sge0split  43918  sge0fodjrnlem  43925  sge0seq  43955  meadjiunlem  43974  meaiuninclem  43989  omeiunle  44026  ovolval2lem  44152  ovolval4lem2  44159  ovolval5lem2  44162  ovolval5lem3  44163  ovolval5  44164  ovnovollem2  44166  smfsuplem2  44313  smfsup  44315  smfsupmpt  44316  smfinf  44319  smfinfmpt  44320  smflimsuplem1  44321  smflimsuplem2  44322  smflimsuplem4  44324  smflimsuplem5  44325  smflimsuplem7  44327  smflimsup  44329  fnrnafv  44622  afv2eq12d  44675