Theorem rneqi 5849

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

Syntax hints:   = wceq 1539  ran crn 5591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-cnv 5598  df-dm 5600  df-rn 5601

This theorem is referenced by:  rnmpt  5867  resima  5928  resima2  5929  mptima  5984  ima0  5988  rnuni  6057  imaundi  6058  imaundir  6059  inimass  6063  dminxp  6088  imainrect  6089  xpima  6090  rnresv  6109  imacnvcnv  6114  rnpropg  6130  imadmres  6142  mptpreima  6146  rnmpt0f  6151  dmco  6162  resdif  6746  fpr  7035  rnmptc  7091  fliftfuns  7194  rnoprab  7387  rnmpo  7416  elrnmpores  7420  curry1  7953  curry2  7956  fparlem3  7963  fparlem4  7964  fsplitfpar  7968  qliftfuns  8602  xpassen  8862  sbthlem6  8884  pwfir  8968  hartogslem1  9310  rnttrcl  9489  rankwflemb  9560  fin23lem34  10111  axcc2lem  10201  axdc2lem  10213  fpwwe2lem12  10407  seqval  13741  0rest  17149  imasdsval2  17236  fulloppc  17647  oppchofcl  17987  oyoncl  17997  gsumwspan  18494  pmtrprfvalrn  19105  psgnsn  19137  psgnprfval2  19140  oppglsm  19256  efgredlemg  19357  efgredlemd  19359  fincygsubgodd  19724  pjdm  20923  pf1rcl  21524  mpfpf1  21526  pf1ind  21530  leordtvallem1  22370  leordtvallem2  22371  leordtval  22373  cnconst2  22443  ptcmplem1  23212  tgpconncomp  23273  fmucndlem  23452  fmucnd  23453  ucnextcn  23465  metustto  23718  metustexhalf  23721  metuust  23725  cfilucfil2  23726  metuel  23729  psmetutop  23732  restmetu  23735  metucn  23736  minveclem5  24606  minvec  24609  ovolgelb  24653  ovoliunlem1  24675  itg1addlem4  24872  itg1addlem4OLD  24873  itg2seq  24916  itg2i1fseq  24929  itg2cnlem1  24935  efifo  25712  logrn  25723  dfrelog  25730  dvrelog  25801  xrlimcnp  26127  iedgedg  27429  edgiedgb  27433  edg0iedg0  27434  uhgrvtxedgiedgb  27515  uspgrf1oedg  27552  usgrf1oedg  27583  usgredg3  27592  ushgredgedg  27605  ushgredgedgloop  27607  usgrexmpledg  27638  0grsubgr  27654  uhgrspan1  27679  usgredgffibi  27700  dfnbgr3  27714  nbupgrres  27740  usgrnbcnvfv  27741  edginwlk  28011  wlkiswwlks2lem4  28246  wlkiswwlks2lem5  28247  clwlkclwwlk  28375  ex-rn  28813  bafval  28975  cnnvba  29050  minveco  29255  abrexexd  30863  imadifxp  30949  lsmsnorb  31588  prsrn  31874  raddcn  31888  pl1cn  31914  esumrnmpt2  32045  sitgclbn  32319  lfuhgr  33088  mvtval  33471  elmsubrn  33499  dfon4  34204  ellines  34463  rnmptsn  35515  f1omptsnlem  35516  icoreresf  35532  ptrest  35785  ovoliunnfl  35828  voliunnfl  35830  rngoueqz  36107  rngonegmn1l  36108  rngonegmn1r  36109  rngoneglmul  36110  rngonegrmul  36111  zerdivemp1x  36114  isdrngo2  36125  rngokerinj  36142  iscrngo2  36164  idlnegcl  36189  1idl  36193  0rngo  36194  smprngopr  36219  prnc  36234  isfldidl  36235  isdmn3  36241  rncnvepres  36446  imaopab  40214  mzpmfp  40576  dmnonrel  41205  imanonrel  41208  cnvrcl0  41240  ntrrn  41739  rnresun  42723  disjinfi  42738  imassmpt  42817  supxrleubrnmptf  42998  elicores  43078  limsupvaluz  43256  limsupmnflem  43268  limsupvaluz2  43286  limsup10ex  43321  liminf10ex  43322  liminflelimsuplem  43323  ioodvbdlimc1lem1  43479  ioodvbdlimc1  43481  ioodvbdlimc2  43483  fourierdlem42  43697  ioorrnopn  43853  subsaliuncl  43904  sge0sn  43924  sge0split  43954  sge0fodjrnlem  43961  sge0xaddlem2  43979  volicorescl  44098  hoidmvlelem3  44142  vonioolem2  44226  smflimsuplem1  44364  smflimsuplem3  44366  smflimsup  44372  fcoreslem2  44569