Theorem rneqi 5890

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

Syntax hints:   = wceq 1540  ran crn 5632

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  rnmpt  5910  resima  5975  resima2  5976  mptima  6032  ima0  6037  rnuni  6109  imaundi  6110  imaundir  6111  inimass  6116  dminxp  6141  imainrect  6142  xpima  6143  rnresv  6162  imacnvcnv  6167  rnpropg  6183  imadmres  6195  mptpreima  6199  rnmpt0f  6204  dmco  6215  resdif  6803  fpr  7108  rnmptc  7163  fliftfuns  7271  rnoprab  7474  rnmpo  7502  elrnmpores  7507  curry1  8060  curry2  8063  fparlem3  8070  fparlem4  8071  fsplitfpar  8074  qliftfuns  8754  xpassen  9012  sbthlem6  9033  pwfir  9242  hartogslem1  9471  rnttrcl  9651  rankwflemb  9722  fin23lem34  10275  axcc2lem  10365  axdc2lem  10377  fpwwe2lem12  10571  seqval  13953  0rest  17368  imasdsval2  17455  fulloppc  17866  oppchofcl  18201  oyoncl  18211  gsumwspan  18755  pmtrprfvalrn  19402  psgnsn  19434  psgnprfval2  19437  oppglsm  19556  efgredlemg  19656  efgredlemd  19658  fincygsubgodd  20028  pjdm  21649  pf1rcl  22269  mpfpf1  22271  pf1ind  22275  leordtvallem1  23130  leordtvallem2  23131  leordtval  23133  cnconst2  23203  ptcmplem1  23972  tgpconncomp  24033  fmucndlem  24211  fmucnd  24212  ucnextcn  24224  metustto  24474  metustexhalf  24477  metuust  24481  cfilucfil2  24482  metuel  24485  psmetutop  24488  restmetu  24491  metucn  24492  minveclem5  25366  minvec  25369  ovolgelb  25414  ovoliunlem1  25436  itg1addlem4  25633  itg2seq  25676  itg2i1fseq  25689  itg2cnlem1  25695  efifo  26489  logrn  26500  dfrelog  26507  dvrelog  26579  xrlimcnp  26911  iedgedg  29030  edgiedgb  29034  edg0iedg0  29035  uhgrvtxedgiedgb  29116  uspgrf1oedg  29153  usgrf1oedg  29187  usgredg3  29196  ushgredgedg  29209  ushgredgedgloop  29211  usgrexmpledg  29242  0grsubgr  29258  uhgrspan1  29283  usgredgffibi  29304  dfnbgr3  29318  nbupgrres  29344  usgrnbcnvfv  29345  edginwlk  29615  wlkiswwlks2lem4  29852  wlkiswwlks2lem5  29853  clwlkclwwlk  29981  ex-rn  30419  bafval  30583  cnnvba  30658  minveco  30863  abrexexd  32488  imadifxp  32580  elrgspn  33213  elrgspnsubrun  33216  lsmsnorb  33355  prsrn  33898  raddcn  33912  pl1cn  33938  esumrnmpt2  34051  sitgclbn  34327  lfuhgr  35098  mvtval  35480  elmsubrn  35508  dfon4  35874  ellines  36133  rnmptsn  37316  f1omptsnlem  37317  icoreresf  37333  ptrest  37606  ovoliunnfl  37649  voliunnfl  37651  rngoueqz  37927  rngonegmn1l  37928  rngonegmn1r  37929  rngoneglmul  37930  rngonegrmul  37931  zerdivemp1x  37934  isdrngo2  37945  rngokerinj  37962  iscrngo2  37984  idlnegcl  38009  1idl  38013  0rngo  38014  smprngopr  38039  prnc  38054  isfldidl  38055  isdmn3  38061  rncnvepres  38284  imaopab  42212  mzpmfp  42728  dmnonrel  43572  imanonrel  43575  cnvrcl0  43607  ntrrn  44104  modelaxreplem2  44962  modelaxreplem3  44963  rnresun  45167  disjinfi  45179  imassmpt  45249  supxrleubrnmptf  45440  elicores  45524  limsupvaluz  45699  limsupmnflem  45711  limsupvaluz2  45729  limsup10ex  45764  liminf10ex  45765  liminflelimsuplem  45766  ioodvbdlimc1lem1  45922  ioodvbdlimc1  45924  ioodvbdlimc2  45926  fourierdlem42  46140  ioorrnopn  46296  subsaliuncl  46349  sge0sn  46370  sge0split  46400  sge0fodjrnlem  46407  sge0xaddlem2  46425  volicorescl  46544  hoidmvlelem3  46588  vonioolem2  46672  smflimsuplem1  46811  smflimsuplem3  46813  smflimsup  46819  fcoreslem2  47058  dfclnbgr3  47820  isuspgrim0lem  47886  upgrimtrlslem2  47898  usgrexmpl1edg  48008  usgrexmpl2edg  48013