Theorem rneqi 5922

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

Syntax hints:   = wceq 1540  ran crn 5660

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is referenced by:  rnmpt  5942  resima  6007  resima2  6008  mptima  6064  ima0  6069  rnuni  6142  imaundi  6143  imaundir  6144  inimass  6149  dminxp  6174  imainrect  6175  xpima  6176  rnresv  6195  imacnvcnv  6200  rnpropg  6216  imadmres  6228  mptpreima  6232  rnmpt0f  6237  dmco  6248  resdif  6844  fpr  7149  rnmptc  7204  fliftfuns  7312  rnoprab  7517  rnmpo  7545  elrnmpores  7550  curry1  8108  curry2  8111  fparlem3  8118  fparlem4  8119  fsplitfpar  8122  qliftfuns  8823  xpassen  9085  sbthlem6  9107  pwfir  9332  hartogslem1  9561  rnttrcl  9741  rankwflemb  9812  fin23lem34  10365  axcc2lem  10455  axdc2lem  10467  fpwwe2lem12  10661  seqval  14035  0rest  17448  imasdsval2  17535  fulloppc  17942  oppchofcl  18277  oyoncl  18287  gsumwspan  18829  pmtrprfvalrn  19474  psgnsn  19506  psgnprfval2  19509  oppglsm  19628  efgredlemg  19728  efgredlemd  19730  fincygsubgodd  20100  pjdm  21672  pf1rcl  22292  mpfpf1  22294  pf1ind  22298  leordtvallem1  23153  leordtvallem2  23154  leordtval  23156  cnconst2  23226  ptcmplem1  23995  tgpconncomp  24056  fmucndlem  24234  fmucnd  24235  ucnextcn  24247  metustto  24497  metustexhalf  24500  metuust  24504  cfilucfil2  24505  metuel  24508  psmetutop  24511  restmetu  24514  metucn  24515  minveclem5  25390  minvec  25393  ovolgelb  25438  ovoliunlem1  25460  itg1addlem4  25657  itg2seq  25700  itg2i1fseq  25713  itg2cnlem1  25719  efifo  26513  logrn  26524  dfrelog  26531  dvrelog  26603  xrlimcnp  26935  iedgedg  29034  edgiedgb  29038  edg0iedg0  29039  uhgrvtxedgiedgb  29120  uspgrf1oedg  29157  usgrf1oedg  29191  usgredg3  29200  ushgredgedg  29213  ushgredgedgloop  29215  usgrexmpledg  29246  0grsubgr  29262  uhgrspan1  29287  usgredgffibi  29308  dfnbgr3  29322  nbupgrres  29348  usgrnbcnvfv  29349  edginwlk  29620  wlkiswwlks2lem4  29859  wlkiswwlks2lem5  29860  clwlkclwwlk  29988  ex-rn  30426  bafval  30590  cnnvba  30665  minveco  30870  abrexexd  32495  imadifxp  32587  elrgspn  33246  elrgspnsubrun  33249  lsmsnorb  33411  prsrn  33951  raddcn  33965  pl1cn  33991  esumrnmpt2  34104  sitgclbn  34380  lfuhgr  35145  mvtval  35527  elmsubrn  35555  dfon4  35916  ellines  36175  rnmptsn  37358  f1omptsnlem  37359  icoreresf  37375  ptrest  37648  ovoliunnfl  37691  voliunnfl  37693  rngoueqz  37969  rngonegmn1l  37970  rngonegmn1r  37971  rngoneglmul  37972  rngonegrmul  37973  zerdivemp1x  37976  isdrngo2  37987  rngokerinj  38004  iscrngo2  38026  idlnegcl  38051  1idl  38055  0rngo  38056  smprngopr  38081  prnc  38096  isfldidl  38097  isdmn3  38103  rncnvepres  38326  imaopab  42249  mzpmfp  42737  dmnonrel  43581  imanonrel  43584  cnvrcl0  43616  ntrrn  44113  modelaxreplem2  44971  modelaxreplem3  44972  rnresun  45171  disjinfi  45183  imassmpt  45253  supxrleubrnmptf  45445  elicores  45529  limsupvaluz  45704  limsupmnflem  45716  limsupvaluz2  45734  limsup10ex  45769  liminf10ex  45770  liminflelimsuplem  45771  ioodvbdlimc1lem1  45927  ioodvbdlimc1  45929  ioodvbdlimc2  45931  fourierdlem42  46145  ioorrnopn  46301  subsaliuncl  46354  sge0sn  46375  sge0split  46405  sge0fodjrnlem  46412  sge0xaddlem2  46430  volicorescl  46549  hoidmvlelem3  46593  vonioolem2  46677  smflimsuplem1  46816  smflimsuplem3  46818  smflimsup  46824  fcoreslem2  47060  dfclnbgr3  47807  isuspgrim0lem  47873  upgrimtrlslem2  47885  usgrexmpl1edg  47995  usgrexmpl2edg  48000