Theorem rneqi 5884

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

Syntax hints:   = wceq 1541  ran crn 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-cnv 5630  df-dm 5632  df-rn 5633

This theorem is referenced by:  rnmpt  5904  resima  5972  resima2  5973  mptima  6029  ima0  6034  rnuni  6104  imaundi  6105  imaundir  6106  inimass  6111  dminxp  6136  imainrect  6137  xpima  6138  rnresv  6157  imacnvcnv  6162  rnpropg  6178  imadmres  6190  mptpreima  6194  rnmpt0f  6199  dmco  6211  resdif  6793  fpr  7097  rnmptc  7151  fliftfuns  7258  rnoprab  7461  rnmpo  7489  elrnmpores  7494  curry1  8044  curry2  8047  fparlem3  8054  fparlem4  8055  fsplitfpar  8058  qliftfuns  8739  xpassen  8997  sbthlem6  9018  pwfir  9215  hartogslem1  9445  rnttrcl  9629  rankwflemb  9703  fin23lem34  10254  axcc2lem  10344  axdc2lem  10356  fpwwe2lem12  10551  seqval  13933  0rest  17347  imasdsval2  17435  fulloppc  17846  oppchofcl  18181  oyoncl  18191  gsumwspan  18769  pmtrprfvalrn  19415  psgnsn  19447  psgnprfval2  19450  oppglsm  19569  efgredlemg  19669  efgredlemd  19671  fincygsubgodd  20041  pjdm  21660  pf1rcl  22291  mpfpf1  22293  pf1ind  22297  leordtvallem1  23152  leordtvallem2  23153  leordtval  23155  cnconst2  23225  ptcmplem1  23994  tgpconncomp  24055  fmucndlem  24232  fmucnd  24233  ucnextcn  24245  metustto  24495  metustexhalf  24498  metuust  24502  cfilucfil2  24503  metuel  24506  psmetutop  24509  restmetu  24512  metucn  24513  minveclem5  25387  minvec  25390  ovolgelb  25435  ovoliunlem1  25457  itg1addlem4  25654  itg2seq  25697  itg2i1fseq  25710  itg2cnlem1  25716  efifo  26510  logrn  26521  dfrelog  26528  dvrelog  26600  xrlimcnp  26932  iedgedg  29072  edgiedgb  29076  edg0iedg0  29077  uhgrvtxedgiedgb  29158  uspgrf1oedg  29195  usgrf1oedg  29229  usgredg3  29238  ushgredgedg  29251  ushgredgedgloop  29253  usgrexmpledg  29284  0grsubgr  29300  uhgrspan1  29325  usgredgffibi  29346  dfnbgr3  29360  nbupgrres  29386  usgrnbcnvfv  29387  edginwlk  29657  wlkiswwlks2lem4  29894  wlkiswwlks2lem5  29895  clwlkclwwlk  30026  ex-rn  30464  bafval  30628  cnnvba  30703  minveco  30908  abrexexd  32533  imadifxp  32625  elrgspn  33277  elrgspnsubrun  33280  lsmsnorb  33421  prsrn  34021  raddcn  34035  pl1cn  34061  esumrnmpt2  34174  sitgclbn  34449  lfuhgr  35261  mvtval  35643  elmsubrn  35671  dfon4  36034  ellines  36295  rnmptsn  37479  f1omptsnlem  37480  icoreresf  37496  ptrest  37759  ovoliunnfl  37802  voliunnfl  37804  rngoueqz  38080  rngonegmn1l  38081  rngonegmn1r  38082  rngoneglmul  38083  rngonegrmul  38084  zerdivemp1x  38087  isdrngo2  38098  rngokerinj  38115  iscrngo2  38137  idlnegcl  38162  1idl  38166  0rngo  38167  smprngopr  38192  prnc  38207  isfldidl  38208  isdmn3  38214  rncnvepres  38441  dfsuccl2  38583  imaopab  42429  mzpmfp  42931  dmnonrel  43773  imanonrel  43776  cnvrcl0  43808  ntrrn  44305  modelaxreplem2  45162  modelaxreplem3  45163  rnresun  45366  disjinfi  45378  imassmpt  45448  supxrleubrnmptf  45637  elicores  45721  limsupvaluz  45894  limsupmnflem  45906  limsupvaluz2  45924  limsup10ex  45959  liminf10ex  45960  liminflelimsuplem  45961  ioodvbdlimc1lem1  46117  ioodvbdlimc1  46119  ioodvbdlimc2  46121  fourierdlem42  46335  ioorrnopn  46491  subsaliuncl  46544  sge0sn  46565  sge0split  46595  sge0fodjrnlem  46602  sge0xaddlem2  46620  volicorescl  46739  hoidmvlelem3  46783  vonioolem2  46867  smflimsuplem1  47006  smflimsuplem3  47008  smflimsup  47014  fcoreslem2  47252  dfclnbgr3  48014  isuspgrim0lem  48081  upgrimtrlslem2  48093  usgrexmpl1edg  48212  usgrexmpl2edg  48217