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  17862  oppchofcl  18197  oyoncl  18207  gsumwspan  18749  pmtrprfvalrn  19394  psgnsn  19426  psgnprfval2  19429  oppglsm  19548  efgredlemg  19648  efgredlemd  19650  fincygsubgodd  20020  pjdm  21592  pf1rcl  22212  mpfpf1  22214  pf1ind  22218  leordtvallem1  23073  leordtvallem2  23074  leordtval  23076  cnconst2  23146  ptcmplem1  23915  tgpconncomp  23976  fmucndlem  24154  fmucnd  24155  ucnextcn  24167  metustto  24417  metustexhalf  24420  metuust  24424  cfilucfil2  24425  metuel  24428  psmetutop  24431  restmetu  24434  metucn  24435  minveclem5  25309  minvec  25312  ovolgelb  25357  ovoliunlem1  25379  itg1addlem4  25576  itg2seq  25619  itg2i1fseq  25632  itg2cnlem1  25638  efifo  26432  logrn  26443  dfrelog  26450  dvrelog  26522  xrlimcnp  26854  iedgedg  28953  edgiedgb  28957  edg0iedg0  28958  uhgrvtxedgiedgb  29039  uspgrf1oedg  29076  usgrf1oedg  29110  usgredg3  29119  ushgredgedg  29132  ushgredgedgloop  29134  usgrexmpledg  29165  0grsubgr  29181  uhgrspan1  29206  usgredgffibi  29227  dfnbgr3  29241  nbupgrres  29267  usgrnbcnvfv  29268  edginwlk  29538  wlkiswwlks2lem4  29775  wlkiswwlks2lem5  29776  clwlkclwwlk  29904  ex-rn  30342  bafval  30506  cnnvba  30581  minveco  30786  abrexexd  32411  imadifxp  32503  elrgspn  33170  elrgspnsubrun  33173  lsmsnorb  33335  prsrn  33878  raddcn  33892  pl1cn  33918  esumrnmpt2  34031  sitgclbn  34307  lfuhgr  35078  mvtval  35460  elmsubrn  35488  dfon4  35854  ellines  36113  rnmptsn  37296  f1omptsnlem  37297  icoreresf  37313  ptrest  37586  ovoliunnfl  37629  voliunnfl  37631  rngoueqz  37907  rngonegmn1l  37908  rngonegmn1r  37909  rngoneglmul  37910  rngonegrmul  37911  zerdivemp1x  37914  isdrngo2  37925  rngokerinj  37942  iscrngo2  37964  idlnegcl  37989  1idl  37993  0rngo  37994  smprngopr  38019  prnc  38034  isfldidl  38035  isdmn3  38041  rncnvepres  38264  imaopab  42192  mzpmfp  42708  dmnonrel  43552  imanonrel  43555  cnvrcl0  43587  ntrrn  44084  modelaxreplem2  44942  modelaxreplem3  44943  rnresun  45147  disjinfi  45159  imassmpt  45229  supxrleubrnmptf  45420  elicores  45504  limsupvaluz  45679  limsupmnflem  45691  limsupvaluz2  45709  limsup10ex  45744  liminf10ex  45745  liminflelimsuplem  45746  ioodvbdlimc1lem1  45902  ioodvbdlimc1  45904  ioodvbdlimc2  45906  fourierdlem42  46120  ioorrnopn  46276  subsaliuncl  46329  sge0sn  46350  sge0split  46380  sge0fodjrnlem  46387  sge0xaddlem2  46405  volicorescl  46524  hoidmvlelem3  46568  vonioolem2  46652  smflimsuplem1  46791  smflimsuplem3  46793  smflimsup  46799  fcoreslem2  47038  dfclnbgr3  47800  isuspgrim0lem  47866  upgrimtrlslem2  47878  usgrexmpl1edg  47988  usgrexmpl2edg  47993