Theorem rneqi 5921

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

This proof depends on syntax axioms:   = wceq 1570  ran crn 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-cnv 5663  df-dm 5665  df-rn 5666

This theorem is used by:  rnmpt  5941  resima  6008  resima2  6009  mptima  6068  ima0  6073  rnuni  6140  imaundi  6141  imaundir  6142  inimass  6146  dminxp  6173  imainrect  6174  xpima  6175  rnresv  6195  imadifssran  6197  imacnvcnv  6202  rnpropg  6218  imadmres  6230  mptpreima  6234  rnmpt0f  6239  dmco  6251  resdif  6840  fpr  7152  rnmptc  7207  fliftfuns  7316  rnoprab  7519  rnmpo  7547  elrnmpores  7552  curry1  8102  curry2  8105  fparlem3  8112  fparlem4  8113  fsplitfpar  8116  qliftfuns  8805  xpassen  9070  sbthlem6  9091  pwfir  9287  hartogslem1  9515  rnttrcl  9702  rankwflemb  9776  fin23lem34  10349  axcc2lem  10439  axdc2lem  10451  fpwwe2lem12  10652  seqval  14077  0rest  17515  imasdsval2  17603  fulloppc  18014  oppchofcl  18349  oyoncl  18359  gsumwspan  18956  pmtrprfvalrn  19616  psgnsn  19648  psgnprfval2  19651  oppglsm  19770  efgredlemg  19870  efgredlemd  19872  fincygsubgodd  20242  pjdm  21921  pf1rcl  22575  mpfpf1  22577  pf1ind  22581  leordtvallem1  23436  leordtvallem2  23437  leordtval  23439  cnconst2  23509  ptcmplem1  24279  tgpconncomp  24340  fmucndlem  24517  fmucnd  24518  ucnextcn  24530  metustto  24780  metustexhalf  24783  metuust  24787  cfilucfil2  24788  metuel  24791  psmetutop  24794  restmetu  24797  metucn  24798  minveclem5  25662  minvec  25665  ovolgelb  25709  ovoliunlem1  25731  itg1addlem4  25928  itg2seq  25971  itg2i1fseq  25984  itg2cnlem1  25990  efifo  26785  logrn  26796  dfrelog  26803  dvrelog  26875  xrlimcnp  27206  iedgedg  29508  edgiedgb  29512  edg0iedg0  29513  uhgrvtxedgiedgb  29594  lfuhgr  29606  uspgrf1oedg  29634  usgrf1oedg  29668  usgredg3  29677  ushgredgedg  29690  ushgredgedgloop  29692  usgrexmpledg  29723  0grsubgr  29739  uhgrspan1  29764  usgredgffibi  29785  dfnbgr3  29799  nbupgrres  29825  usgrnbcnvfv  29826  edginwlk  30095  wlkiswwlks2lem4  30341  wlkiswwlks2lem5  30342  clwlkclwwlk  30473  ex-rn  30921  bafval  31086  cnnvba  31161  minveco  31366  abrexexd  32985  imadifxp  33075  elrgspn  33687  elrgspnsubrun  33690  lsmsnorb  33825  prsrn  34426  raddcn  34440  pl1cn  34466  esumrnmpt2  34579  sitgclbn  34855  mvtval  36080  elmsubrn  36108  dfon4  36471  ellines  36733  rnmptsn  38090  f1omptsnlem  38091  icoreresf  38107  ptrest  38369  ovoliunnfl  38412  voliunnfl  38414  rngoueqz  38691  rngonegmn1l  38692  rngonegmn1r  38693  rngoneglmul  38694  rngonegrmul  38695  zerdivemp1x  38698  isdrngo2  38709  rngokerinj  38726  iscrngo2  38748  idlnegcl  38773  1idl  38777  0rngo  38778  smprngopr  38803  prnc  38818  isfldidl  38819  isdmn3  38825  rncnvepres  39058  rnqmap  39203  dfsuccl2  39219  imaopab  43102  mzpmfp  43593  dmnonrel  44431  imanonrel  44434  cnvrcl0  44466  ntrrn  44963  modelaxreplem2  45803  modelaxreplem3  45804  rnresun  46013  disjinfi  46025  imassmpt  46092  supxrleubrnmptf  46280  elicores  46364  limsupvaluz  46537  limsupmnflem  46549  limsupvaluz2  46567  limsup10ex  46602  liminf10ex  46603  liminflelimsuplem  46604  ioodvbdlimc1lem1  46760  ioodvbdlimc1  46762  ioodvbdlimc2  46764  fourierdlem42  46978  ioorrnopn  47134  subsaliuncl  47187  sge0sn  47208  sge0split  47238  sge0fodjrnlem  47245  sge0xaddlem2  47263  volicorescl  47382  hoidmvlelem3  47426  vonioolem2  47510  smflimsuplem1  47649  smflimsuplem3  47651  smflimsup  47657  fcoreslem2  47953  dfclnbgr3  48743  isuspgrim0lem  48810  upgrimtrlslem2  48822  usgrexmpl1edg  48941  usgrexmpl2edg  48946