Theorem rneqi 5835

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

Syntax hints:   = wceq 1539  ran crn 5581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-cnv 5588  df-dm 5590  df-rn 5591

This theorem is referenced by:  rnmpt  5853  resima  5914  resima2  5915  mptima  5970  ima0  5974  rnuni  6041  imaundi  6042  imaundir  6043  inimass  6047  dminxp  6072  imainrect  6073  xpima  6074  rnresv  6093  imacnvcnv  6098  rnpropg  6114  imadmres  6126  mptpreima  6130  rnmpt0f  6135  dmco  6147  resdif  6720  fpr  7008  rnmptc  7064  fliftfuns  7165  rnoprab  7356  rnmpo  7385  elrnmpores  7389  curry1  7915  curry2  7918  fparlem3  7925  fparlem4  7926  fsplitfpar  7930  qliftfuns  8551  xpassen  8806  sbthlem6  8828  pwfir  8921  hartogslem1  9231  rankwflemb  9482  fin23lem34  10033  axcc2lem  10123  axdc2lem  10135  fpwwe2lem12  10329  seqval  13660  0rest  17057  imasdsval2  17144  fulloppc  17554  oppchofcl  17894  oyoncl  17904  gsumwspan  18400  pmtrprfvalrn  19011  psgnsn  19043  psgnprfval2  19046  oppglsm  19162  efgredlemg  19263  efgredlemd  19265  fincygsubgodd  19630  pjdm  20824  pf1rcl  21425  mpfpf1  21427  pf1ind  21431  leordtvallem1  22269  leordtvallem2  22270  leordtval  22272  cnconst2  22342  ptcmplem1  23111  tgpconncomp  23172  fmucndlem  23351  fmucnd  23352  ucnextcn  23364  metustto  23615  metustexhalf  23618  metuust  23622  cfilucfil2  23623  metuel  23626  psmetutop  23629  restmetu  23632  metucn  23633  minveclem5  24502  minvec  24505  ovolgelb  24549  ovoliunlem1  24571  itg1addlem4  24768  itg1addlem4OLD  24769  itg2seq  24812  itg2i1fseq  24825  itg2cnlem1  24831  efifo  25608  logrn  25619  dfrelog  25626  dvrelog  25697  xrlimcnp  26023  iedgedg  27323  edgiedgb  27327  edg0iedg0  27328  uhgrvtxedgiedgb  27409  uspgrf1oedg  27446  usgrf1oedg  27477  usgredg3  27486  ushgredgedg  27499  ushgredgedgloop  27501  usgrexmpledg  27532  0grsubgr  27548  uhgrspan1  27573  usgredgffibi  27594  dfnbgr3  27608  nbupgrres  27634  usgrnbcnvfv  27635  edginwlk  27904  wlkiswwlks2lem4  28138  wlkiswwlks2lem5  28139  clwlkclwwlk  28267  ex-rn  28705  bafval  28867  cnnvba  28942  minveco  29147  abrexexd  30755  imadifxp  30841  lsmsnorb  31481  prsrn  31767  raddcn  31781  pl1cn  31807  esumrnmpt2  31936  sitgclbn  32210  lfuhgr  32979  mvtval  33362  elmsubrn  33390  rnttrcl  33708  dfon4  34122  ellines  34381  rnmptsn  35433  f1omptsnlem  35434  icoreresf  35450  ptrest  35703  ovoliunnfl  35746  voliunnfl  35748  rngoueqz  36025  rngonegmn1l  36026  rngonegmn1r  36027  rngoneglmul  36028  rngonegrmul  36029  zerdivemp1x  36032  isdrngo2  36043  rngokerinj  36060  iscrngo2  36082  idlnegcl  36107  1idl  36111  0rngo  36112  smprngopr  36137  prnc  36152  isfldidl  36153  isdmn3  36159  rncnvepres  36366  imaopab  40133  mzpmfp  40485  dmnonrel  41087  imanonrel  41090  cnvrcl0  41122  ntrrn  41621  rnresun  42605  disjinfi  42620  imassmpt  42699  supxrleubrnmptf  42881  elicores  42961  limsupvaluz  43139  limsupmnflem  43151  limsupvaluz2  43169  limsup10ex  43204  liminf10ex  43205  liminflelimsuplem  43206  ioodvbdlimc1lem1  43362  ioodvbdlimc1  43364  ioodvbdlimc2  43366  fourierdlem42  43580  ioorrnopn  43736  subsaliuncl  43787  sge0sn  43807  sge0split  43837  sge0fodjrnlem  43844  sge0xaddlem2  43862  volicorescl  43981  hoidmvlelem3  44025  vonioolem2  44109  smflimsuplem1  44240  smflimsuplem3  44242  smflimsup  44248  fcoreslem2  44445