Theorem rneqi 5928

Description: Equality inference for range. (Contributed by NM, 4-Mar-2004.)

Hypothesis

Ref	Expression
rneqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
rneqi	⊢ ran 𝐴 = ran 𝐵

Proof of Theorem rneqi

Step	Hyp	Ref	Expression
1		rneqi.1	. 2 ⊢ 𝐴 = 𝐵
2		rneq 5927	. 2 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
3	1, 2	ax-mp 5	1 ⊢ ran 𝐴 = ran 𝐵

Syntax hints:   = wceq 1567  ran crn 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-cnv 5670  df-dm 5672  df-rn 5673

This theorem is referenced by:  rnmpt  5948  resima  6015  resima2  6016  mptima  6075  ima0  6080  rnuni  6147  imaundi  6148  imaundir  6149  inimass  6153  dminxp  6179  imainrect  6180  xpima  6181  rnresv  6201  imadifssran  6203  imacnvcnv  6208  rnpropg  6224  imadmres  6236  mptpreima  6240  rnmpt0f  6245  dmco  6257  resdif  6843  fpr  7152  rnmptc  7206  fliftfuns  7313  rnoprab  7516  rnmpo  7544  elrnmpores  7549  curry1  8098  curry2  8101  fparlem3  8108  fparlem4  8109  fsplitfpar  8112  qliftfuns  8801  xpassen  9058  sbthlem6  9079  pwfir  9275  hartogslem1  9503  rnttrcl  9690  rankwflemb  9764  fin23lem34  10329  axcc2lem  10419  axdc2lem  10431  fpwwe2lem12  10626  seqval  14047  0rest  17481  imasdsval2  17569  fulloppc  17980  oppchofcl  18315  oyoncl  18325  gsumwspan  18904  pmtrprfvalrn  19557  psgnsn  19589  psgnprfval2  19592  oppglsm  19711  efgredlemg  19811  efgredlemd  19813  fincygsubgodd  20183  pjdm  21825  pf1rcl  22477  mpfpf1  22479  pf1ind  22483  leordtvallem1  23335  leordtvallem2  23336  leordtval  23338  cnconst2  23408  ptcmplem1  24177  tgpconncomp  24238  fmucndlem  24415  fmucnd  24416  ucnextcn  24428  metustto  24678  metustexhalf  24681  metuust  24685  cfilucfil2  24686  metuel  24689  psmetutop  24692  restmetu  24695  metucn  24696  minveclem5  25560  minvec  25563  ovolgelb  25607  ovoliunlem1  25629  itg1addlem4  25826  itg2seq  25869  itg2i1fseq  25882  itg2cnlem1  25888  efifo  26677  logrn  26688  dfrelog  26695  dvrelog  26767  xrlimcnp  27098  iedgedg  29340  edgiedgb  29344  edg0iedg0  29345  uhgrvtxedgiedgb  29426  uspgrf1oedg  29463  usgrf1oedg  29497  usgredg3  29506  ushgredgedg  29519  ushgredgedgloop  29521  usgrexmpledg  29552  0grsubgr  29568  uhgrspan1  29593  usgredgffibi  29614  dfnbgr3  29628  nbupgrres  29654  usgrnbcnvfv  29655  edginwlk  29924  wlkiswwlks2lem4  30161  wlkiswwlks2lem5  30162  clwlkclwwlk  30293  ex-rn  30731  bafval  30896  cnnvba  30971  minveco  31176  abrexexd  32795  imadifxp  32886  elrgspn  33506  elrgspnsubrun  33509  lsmsnorb  33647  prsrn  34249  raddcn  34263  pl1cn  34289  esumrnmpt2  34402  sitgclbn  34677  lfuhgr  35508  mvtval  35890  elmsubrn  35918  dfon4  36281  ellines  36542  rnmptsn  37868  f1omptsnlem  37869  icoreresf  37885  ptrest  38157  ovoliunnfl  38200  voliunnfl  38202  rngoueqz  38478  rngonegmn1l  38479  rngonegmn1r  38480  rngoneglmul  38481  rngonegrmul  38482  zerdivemp1x  38485  isdrngo2  38496  rngokerinj  38513  iscrngo2  38535  idlnegcl  38560  1idl  38564  0rngo  38565  smprngopr  38590  prnc  38605  isfldidl  38606  isdmn3  38612  rncnvepres  38847  rnqmap  38992  dfsuccl2  39008  imaopab  42891  mzpmfp  43369  dmnonrel  44207  imanonrel  44210  cnvrcl0  44242  ntrrn  44739  modelaxreplem2  45579  modelaxreplem3  45580  rnresun  45789  disjinfi  45801  imassmpt  45868  supxrleubrnmptf  46056  elicores  46140  limsupvaluz  46313  limsupmnflem  46325  limsupvaluz2  46343  limsup10ex  46378  liminf10ex  46379  liminflelimsuplem  46380  ioodvbdlimc1lem1  46536  ioodvbdlimc1  46538  ioodvbdlimc2  46540  fourierdlem42  46754  ioorrnopn  46910  subsaliuncl  46963  sge0sn  46984  sge0split  47014  sge0fodjrnlem  47021  sge0xaddlem2  47039  volicorescl  47158  hoidmvlelem3  47202  vonioolem2  47286  smflimsuplem1  47425  smflimsuplem3  47427  smflimsup  47433  fcoreslem2  47689  dfclnbgr3  48479  isuspgrim0lem  48546  upgrimtrlslem2  48558  usgrexmpl1edg  48677  usgrexmpl2edg  48682