Theorem rneqd 5934

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

Syntax hints:   → wi 4   = wceq 1534  ran crn 5673

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5143  df-opab 5205  df-cnv 5680  df-dm 5682  df-rn 5683

This theorem is referenced by:  resima2  6014  imaeq1  6052  imaeq2  6053  mptimass  6070  resiima  6073  rnxpid  6171  xpima  6180  funimacnv  6628  fnima  6679  focofo  6818  rnfvprc  6885  elimampo  7552  elxp4  7924  elxp5  7925  2ndval  7990  fo2nd  8008  f2ndres  8012  curry1  8103  curry2  8106  oarec  8576  en1  9037  en1OLD  9038  xpassen  9082  xpdom2  9083  sbthlem4  9102  fodomr  9144  dffi3  9446  marypha2lem4  9453  ordtypelem9  9541  dfac12lem1  10158  dfac12r  10161  fin23lem32  10359  fin23lem34  10361  fin23lem35  10362  fin23lem36  10363  fin23lem38  10364  fin23lem39  10365  fin23lem41  10367  itunitc  10436  ttukeylem3  10526  fpwwe2lem5  10650  fpwwe2lem8  10653  wunex2  10753  wuncval2  10762  gruima  10817  rpnnen1lem6  12988  hashf1lem1  14439  hashf1lem1OLD  14440  s1rn  14573  relexprng  15017  relexprnd  15019  relexpfld  15020  limsupval  15442  vdwapfval  16931  vdwapval  16933  vdwmc  16938  vdwpc  16940  vdwlem6  16946  vdwlem8  16948  restval  17399  restid2  17403  prdsval  17428  prdsdsval  17451  prdsdsval2  17457  prdsdsval3  17458  imasval  17484  imasdsval  17488  isfull  17890  arwval  18023  gsumvalx  18627  conjsubg  19195  psgnfval  19446  sylow1lem2  19545  sylow1lem4  19547  sylow1  19549  sylow2blem1  19566  sylow2b  19569  sylow3lem1  19573  sylow3lem2  19574  sylow3lem3  19575  sylow3lem5  19577  sylow3lem6  19578  sylow3  19579  lsmfval  19584  lsmvalx  19585  oppglsm  19588  subglsm  19619  lsmpropd  19623  efgval2  19670  efgi2  19671  efgtlen  19672  efgsdm  19676  efgsdmi  19678  efgsrel  19680  efgs1b  19682  efgsp1  19683  efgsres  19684  efgsfo  19685  efgrelexlemb  19696  frgpnabllem1  19819  iscyg  19825  iscyggen  19826  gsumxp  19922  dprdval  19951  ablfac2  20037  rnrhmsubrg  20533  zncyg  21469  cygznlem2a  21488  frlmsplit2  21694  evlseu  22016  tgrest  23050  ordtval  23080  ordtbas2  23082  ordtcnv  23092  ordtrest  23093  ordtrest2  23095  ispnrm  23230  cmpfi  23299  txval  23455  xkoval  23478  ptval2  23492  ptpjopn  23503  xkoccn  23510  xkoptsub  23545  xkopt  23546  fmval  23834  fmf  23836  txflf  23897  cnextf  23957  subgntr  23998  opnsubg  23999  clsnsg  24001  snclseqg  24007  tsmsval2  24021  tsmsxplem1  24044  ustuqtoplem  24131  utopsnneiplem  24139  utopsnneip  24140  fmucndlem  24183  ressprdsds  24264  mopnval  24331  metuval  24445  metdsval  24750  lebnumlem1  24874  lebnumlem3  24876  pi1xfrcnvlem  24970  pi1xfrcnv  24971  minveclem3b  25343  elovolmr  25392  ovolctb  25406  ovoliunlem3  25420  ovolshftlem1  25425  voliunlem3  25468  voliun  25470  volsup  25472  uniioombllem2  25499  uniioombllem3  25501  mbflimsup  25582  itg1climres  25631  itg2monolem1  25667  itg2i1fseq  25672  itg2cnlem1  25678  ellimc2  25793  dvivth  25930  dvne0  25931  lhop2  25935  lhop  25936  mdegfval  25985  dchrptlem2  27185  dchrpt  27187  seqsval  28148  om2noseqfo  28158  tglnunirn  28339  tgisline  28418  perpln1  28501  perpln2  28502  isperp  28503  ishpg  28550  lmif  28576  islmib  28578  edgval  28849  edgopval  28851  edgstruct  28853  uhgr2edg  29008  usgr1e  29045  cplgrop  29237  cusgrexi  29243  structtocusgr  29246  1loopgredg  29302  1egrvtxdg0  29312  umgr2v2eedg  29325  ex-ima  30239  bafval  30401  pj3i  32005  elimampt  32406  ofrn2  32409  ffsrn  32495  pfxrn2  32645  pfxrn3  32646  swrdrn2  32657  swrdrn3  32658  gsumzresunsn  32746  gsumhashmul  32748  tocycfv  32808  tocycf  32816  trsp2cyc  32822  cycpmco2f1  32823  cycpmco2rn  32824  cycpmconjvlem  32840  cycpmconjslem2  32854  qusbas2  33056  qusima  33058  qusrn  33059  nsgmgc  33062  nsgqusf1olem2  33064  idlsrgval  33150  algextdeglem4  33324  smatrcl  33333  ordtprsval  33455  ordtprsuni  33456  ordtcnvNEW  33457  ordtrestNEW  33458  ordtrest2NEW  33460  qqhval  33511  qqhval2  33519  prodindf  33578  esumval  33601  esumsnf  33619  esumrnmpt2  33623  esumfsupre  33626  esumsup  33644  sxval  33745  omsval  33849  omsfval  33850  carsggect  33874  sibf0  33890  sitgfval  33897  cvmlift3lem6  34870  satfrnmapom  34916  mvtval  35046  mvrsval  35051  mrsubvrs  35068  elmsubrn  35074  msubrn  35075  mstaval  35090  msubvrs  35106  mclsval  35109  filnetlem4  35801  mptsnunlem  36753  dissneqlem  36755  exrecfnlem  36794  ctbssinf  36821  poimirlem3  37031  poimirlem9  37037  poimirlem16  37044  poimirlem17  37045  poimirlem19  37047  poimirlem20  37048  poimirlem24  37052  poimirlem30  37058  poimirlem32  37060  mblfinlem2  37066  ovoliunnfl  37070  voliunnfl  37072  isrngo  37305  drngoi  37359  rngohomval  37372  rngoisoval  37385  idlval  37421  pridlval  37441  maxidlval  37447  igenval  37469  cnvref4  37758  symrelim  37968  unidmqs  38063  lsatset  38399  docaffvalN  40531  docafvalN  40532  aks6d1c2  41533  sticksstones2  41551  sticksstones3  41552  qsalrel  41651  prjcrvfval  41977  mzpmfp  42089  eldiophb  42099  diophrw  42101  tfsconcatrn  42694  rp-tfslim  42705  conrel1d  43016  iunrelexp0  43055  rntrclfv  43085  clsneibex  43455  neicvgbex  43465  rnsnf  44480  fsneqrn  44507  limsupval3  45003  limsupresre  45007  limsupresico  45011  limsuppnfdlem  45012  limsupvaluz  45019  limsupvaluzmpt  45028  limsupvaluz2  45049  supcnvlimsup  45051  supcnvlimsupmpt  45052  liminfval  45070  liminfval5  45076  limsupresxr  45077  liminfresxr  45078  liminfresico  45082  liminfvalxr  45094  fourierdlem60  45477  fourierdlem61  45478  sge0val  45677  sge0z  45686  sge0revalmpt  45689  sge0tsms  45691  sge0sup  45702  sge0split  45720  sge0fodjrnlem  45727  sge0seq  45757  meadjiunlem  45776  meaiuninclem  45791  omeiunle  45828  ovolval2lem  45954  ovolval4lem2  45961  ovolval5lem2  45964  ovolval5lem3  45965  ovolval5  45966  ovnovollem2  45968  smfsuplem2  46123  smfsup  46125  smfsupmpt  46126  smfinf  46129  smfinfmpt  46130  smflimsuplem1  46131  smflimsuplem2  46132  smflimsuplem4  46134  smflimsuplem5  46135  smflimsuplem7  46137  smflimsup  46139  fnrnafv  46465  afv2eq12d  46518