Theorem rneqi 5879

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

Syntax hints:   = wceq 1547  ran crn 5619

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-cnv 5626  df-dm 5628  df-rn 5629

This theorem is referenced by:  rnmpt  5899  resima  5967  resima2  5968  mptima  6024  ima0  6029  rnuni  6099  imaundi  6100  imaundir  6101  inimass  6106  dminxp  6131  imainrect  6132  xpima  6133  rnresv  6152  imacnvcnv  6157  rnpropg  6173  imadmres  6185  mptpreima  6189  rnmpt0f  6194  dmco  6206  resdif  6788  fpr  7097  rnmptc  7151  fliftfuns  7258  rnoprab  7461  rnmpo  7489  elrnmpores  7494  curry1  8043  curry2  8046  fparlem3  8053  fparlem4  8054  fsplitfpar  8057  qliftfuns  8741  xpassen  8999  sbthlem6  9020  pwfir  9217  hartogslem1  9447  rnttrcl  9634  rankwflemb  9708  fin23lem34  10259  axcc2lem  10349  axdc2lem  10361  fpwwe2lem12  10556  seqval  13965  0rest  17383  imasdsval2  17471  fulloppc  17882  oppchofcl  18217  oyoncl  18227  gsumwspan  18805  pmtrprfvalrn  19454  psgnsn  19486  psgnprfval2  19489  oppglsm  19608  efgredlemg  19708  efgredlemd  19710  fincygsubgodd  20080  pjdm  21682  pf1rcl  22335  mpfpf1  22337  pf1ind  22341  leordtvallem1  23193  leordtvallem2  23194  leordtval  23196  cnconst2  23266  ptcmplem1  24035  tgpconncomp  24096  fmucndlem  24273  fmucnd  24274  ucnextcn  24286  metustto  24536  metustexhalf  24539  metuust  24543  cfilucfil2  24544  metuel  24547  psmetutop  24550  restmetu  24553  metucn  24554  minveclem5  25418  minvec  25421  ovolgelb  25465  ovoliunlem1  25487  itg1addlem4  25684  itg2seq  25727  itg2i1fseq  25740  itg2cnlem1  25746  efifo  26529  logrn  26540  dfrelog  26547  dvrelog  26619  xrlimcnp  26950  iedgedg  29137  edgiedgb  29141  edg0iedg0  29142  uhgrvtxedgiedgb  29223  uspgrf1oedg  29260  usgrf1oedg  29294  usgredg3  29303  ushgredgedg  29316  ushgredgedgloop  29318  usgrexmpledg  29349  0grsubgr  29365  uhgrspan1  29390  usgredgffibi  29411  dfnbgr3  29425  nbupgrres  29451  usgrnbcnvfv  29452  edginwlk  29721  wlkiswwlks2lem4  29958  wlkiswwlks2lem5  29959  clwlkclwwlk  30090  ex-rn  30528  bafval  30693  cnnvba  30768  minveco  30973  abrexexd  32597  imadifxp  32690  elrgspn  33327  elrgspnsubrun  33330  lsmsnorb  33474  prsrn  34099  raddcn  34113  pl1cn  34139  esumrnmpt2  34252  sitgclbn  34527  lfuhgr  35346  mvtval  35728  elmsubrn  35756  dfon4  36119  ellines  36380  rnmptsn  37697  f1omptsnlem  37698  icoreresf  37714  ptrest  37986  ovoliunnfl  38029  voliunnfl  38031  rngoueqz  38307  rngonegmn1l  38308  rngonegmn1r  38309  rngoneglmul  38310  rngonegrmul  38311  zerdivemp1x  38314  isdrngo2  38325  rngokerinj  38342  iscrngo2  38364  idlnegcl  38389  1idl  38393  0rngo  38394  smprngopr  38419  prnc  38434  isfldidl  38435  isdmn3  38441  rncnvepres  38676  rnqmap  38821  dfsuccl2  38837  imaopab  42718  mzpmfp  43196  dmnonrel  44034  imanonrel  44037  cnvrcl0  44069  ntrrn  44566  modelaxreplem2  45423  modelaxreplem3  45424  rnresun  45627  disjinfi  45639  imassmpt  45706  supxrleubrnmptf  45894  elicores  45978  limsupvaluz  46151  limsupmnflem  46163  limsupvaluz2  46181  limsup10ex  46216  liminf10ex  46217  liminflelimsuplem  46218  ioodvbdlimc1lem1  46374  ioodvbdlimc1  46376  ioodvbdlimc2  46378  fourierdlem42  46592  ioorrnopn  46748  subsaliuncl  46801  sge0sn  46822  sge0split  46852  sge0fodjrnlem  46859  sge0xaddlem2  46877  volicorescl  46996  hoidmvlelem3  47040  vonioolem2  47124  smflimsuplem1  47263  smflimsuplem3  47265  smflimsup  47271  fcoreslem2  47527  dfclnbgr3  48317  isuspgrim0lem  48384  upgrimtrlslem2  48396  usgrexmpl1edg  48515  usgrexmpl2edg  48520