Theorem rneqi 5887

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

Syntax hints:   = wceq 1542  ran crn 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-cnv 5633  df-dm 5635  df-rn 5636

This theorem is referenced by:  rnmpt  5907  resima  5975  resima2  5976  mptima  6032  ima0  6037  rnuni  6107  imaundi  6108  imaundir  6109  inimass  6114  dminxp  6139  imainrect  6140  xpima  6141  rnresv  6160  imacnvcnv  6165  rnpropg  6181  imadmres  6193  mptpreima  6197  rnmpt0f  6202  dmco  6214  resdif  6796  fpr  7102  rnmptc  7156  fliftfuns  7263  rnoprab  7466  rnmpo  7494  elrnmpores  7499  curry1  8048  curry2  8051  fparlem3  8058  fparlem4  8059  fsplitfpar  8062  qliftfuns  8745  xpassen  9003  sbthlem6  9024  pwfir  9221  hartogslem1  9451  rnttrcl  9637  rankwflemb  9711  fin23lem34  10262  axcc2lem  10352  axdc2lem  10364  fpwwe2lem12  10559  seqval  13968  0rest  17386  imasdsval2  17474  fulloppc  17885  oppchofcl  18220  oyoncl  18230  gsumwspan  18808  pmtrprfvalrn  19457  psgnsn  19489  psgnprfval2  19492  oppglsm  19611  efgredlemg  19711  efgredlemd  19713  fincygsubgodd  20083  pjdm  21700  pf1rcl  22327  mpfpf1  22329  pf1ind  22333  leordtvallem1  23188  leordtvallem2  23189  leordtval  23191  cnconst2  23261  ptcmplem1  24030  tgpconncomp  24091  fmucndlem  24268  fmucnd  24269  ucnextcn  24281  metustto  24531  metustexhalf  24534  metuust  24538  cfilucfil2  24539  metuel  24542  psmetutop  24545  restmetu  24548  metucn  24549  minveclem5  25413  minvec  25416  ovolgelb  25460  ovoliunlem1  25482  itg1addlem4  25679  itg2seq  25722  itg2i1fseq  25735  itg2cnlem1  25741  efifo  26527  logrn  26538  dfrelog  26545  dvrelog  26617  xrlimcnp  26948  iedgedg  29136  edgiedgb  29140  edg0iedg0  29141  uhgrvtxedgiedgb  29222  uspgrf1oedg  29259  usgrf1oedg  29293  usgredg3  29302  ushgredgedg  29315  ushgredgedgloop  29317  usgrexmpledg  29348  0grsubgr  29364  uhgrspan1  29389  usgredgffibi  29410  dfnbgr3  29424  nbupgrres  29450  usgrnbcnvfv  29451  edginwlk  29721  wlkiswwlks2lem4  29958  wlkiswwlks2lem5  29959  clwlkclwwlk  30090  ex-rn  30528  bafval  30693  cnnvba  30768  minveco  30973  abrexexd  32597  imadifxp  32689  elrgspn  33325  elrgspnsubrun  33328  lsmsnorb  33469  prsrn  34078  raddcn  34092  pl1cn  34118  esumrnmpt2  34231  sitgclbn  34506  lfuhgr  35319  mvtval  35701  elmsubrn  35729  dfon4  36092  ellines  36353  rnmptsn  37668  f1omptsnlem  37669  icoreresf  37685  ptrest  37957  ovoliunnfl  38000  voliunnfl  38002  rngoueqz  38278  rngonegmn1l  38279  rngonegmn1r  38280  rngoneglmul  38281  rngonegrmul  38282  zerdivemp1x  38285  isdrngo2  38296  rngokerinj  38313  iscrngo2  38335  idlnegcl  38360  1idl  38364  0rngo  38365  smprngopr  38390  prnc  38405  isfldidl  38406  isdmn3  38412  rncnvepres  38647  rnqmap  38792  dfsuccl2  38808  imaopab  42689  mzpmfp  43196  dmnonrel  44038  imanonrel  44041  cnvrcl0  44073  ntrrn  44570  modelaxreplem2  45427  modelaxreplem3  45428  rnresun  45631  disjinfi  45643  imassmpt  45712  supxrleubrnmptf  45900  elicores  45984  limsupvaluz  46157  limsupmnflem  46169  limsupvaluz2  46187  limsup10ex  46222  liminf10ex  46223  liminflelimsuplem  46224  ioodvbdlimc1lem1  46380  ioodvbdlimc1  46382  ioodvbdlimc2  46384  fourierdlem42  46598  ioorrnopn  46754  subsaliuncl  46807  sge0sn  46828  sge0split  46858  sge0fodjrnlem  46865  sge0xaddlem2  46883  volicorescl  47002  hoidmvlelem3  47046  vonioolem2  47130  smflimsuplem1  47269  smflimsuplem3  47271  smflimsup  47277  fcoreslem2  47527  dfclnbgr3  48317  isuspgrim0lem  48384  upgrimtrlslem2  48396  usgrexmpl1edg  48515  usgrexmpl2edg  48520