Theorem rneqi 5901

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 5900	. 2 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
3	1, 2	ax-mp 5	1 ⊢ ran 𝐴 = ran 𝐵

Syntax hints:   = wceq 1540  ran crn 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-cnv 5646  df-dm 5648  df-rn 5649

This theorem is referenced by:  rnmpt  5921  resima  5986  resima2  5987  mptima  6043  ima0  6048  rnuni  6121  imaundi  6122  imaundir  6123  inimass  6128  dminxp  6153  imainrect  6154  xpima  6155  rnresv  6174  imacnvcnv  6179  rnpropg  6195  imadmres  6207  mptpreima  6211  rnmpt0f  6216  dmco  6227  resdif  6821  fpr  7126  rnmptc  7181  fliftfuns  7289  rnoprab  7494  rnmpo  7522  elrnmpores  7527  curry1  8083  curry2  8086  fparlem3  8093  fparlem4  8094  fsplitfpar  8097  qliftfuns  8777  xpassen  9035  sbthlem6  9056  pwfir  9266  hartogslem1  9495  rnttrcl  9675  rankwflemb  9746  fin23lem34  10299  axcc2lem  10389  axdc2lem  10401  fpwwe2lem12  10595  seqval  13977  0rest  17392  imasdsval2  17479  fulloppc  17886  oppchofcl  18221  oyoncl  18231  gsumwspan  18773  pmtrprfvalrn  19418  psgnsn  19450  psgnprfval2  19453  oppglsm  19572  efgredlemg  19672  efgredlemd  19674  fincygsubgodd  20044  pjdm  21616  pf1rcl  22236  mpfpf1  22238  pf1ind  22242  leordtvallem1  23097  leordtvallem2  23098  leordtval  23100  cnconst2  23170  ptcmplem1  23939  tgpconncomp  24000  fmucndlem  24178  fmucnd  24179  ucnextcn  24191  metustto  24441  metustexhalf  24444  metuust  24448  cfilucfil2  24449  metuel  24452  psmetutop  24455  restmetu  24458  metucn  24459  minveclem5  25333  minvec  25336  ovolgelb  25381  ovoliunlem1  25403  itg1addlem4  25600  itg2seq  25643  itg2i1fseq  25656  itg2cnlem1  25662  efifo  26456  logrn  26467  dfrelog  26474  dvrelog  26546  xrlimcnp  26878  iedgedg  28977  edgiedgb  28981  edg0iedg0  28982  uhgrvtxedgiedgb  29063  uspgrf1oedg  29100  usgrf1oedg  29134  usgredg3  29143  ushgredgedg  29156  ushgredgedgloop  29158  usgrexmpledg  29189  0grsubgr  29205  uhgrspan1  29230  usgredgffibi  29251  dfnbgr3  29265  nbupgrres  29291  usgrnbcnvfv  29292  edginwlk  29563  wlkiswwlks2lem4  29802  wlkiswwlks2lem5  29803  clwlkclwwlk  29931  ex-rn  30369  bafval  30533  cnnvba  30608  minveco  30813  abrexexd  32438  imadifxp  32530  elrgspn  33197  elrgspnsubrun  33200  lsmsnorb  33362  prsrn  33905  raddcn  33919  pl1cn  33945  esumrnmpt2  34058  sitgclbn  34334  lfuhgr  35105  mvtval  35487  elmsubrn  35515  dfon4  35881  ellines  36140  rnmptsn  37323  f1omptsnlem  37324  icoreresf  37340  ptrest  37613  ovoliunnfl  37656  voliunnfl  37658  rngoueqz  37934  rngonegmn1l  37935  rngonegmn1r  37936  rngoneglmul  37937  rngonegrmul  37938  zerdivemp1x  37941  isdrngo2  37952  rngokerinj  37969  iscrngo2  37991  idlnegcl  38016  1idl  38020  0rngo  38021  smprngopr  38046  prnc  38061  isfldidl  38062  isdmn3  38068  rncnvepres  38291  imaopab  42219  mzpmfp  42735  dmnonrel  43579  imanonrel  43582  cnvrcl0  43614  ntrrn  44111  modelaxreplem2  44969  modelaxreplem3  44970  rnresun  45174  disjinfi  45186  imassmpt  45256  supxrleubrnmptf  45447  elicores  45531  limsupvaluz  45706  limsupmnflem  45718  limsupvaluz2  45736  limsup10ex  45771  liminf10ex  45772  liminflelimsuplem  45773  ioodvbdlimc1lem1  45929  ioodvbdlimc1  45931  ioodvbdlimc2  45933  fourierdlem42  46147  ioorrnopn  46303  subsaliuncl  46356  sge0sn  46377  sge0split  46407  sge0fodjrnlem  46414  sge0xaddlem2  46432  volicorescl  46551  hoidmvlelem3  46595  vonioolem2  46679  smflimsuplem1  46818  smflimsuplem3  46820  smflimsup  46826  fcoreslem2  47062  dfclnbgr3  47824  isuspgrim0lem  47890  upgrimtrlslem2  47902  usgrexmpl1edg  48012  usgrexmpl2edg  48017