Theorem rneqi 5948

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

Syntax hints:   = wceq 1540  ran crn 5686

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-cnv 5693  df-dm 5695  df-rn 5696

This theorem is referenced by:  rnmpt  5968  resima  6033  resima2  6034  mptima  6090  ima0  6095  rnuni  6168  imaundi  6169  imaundir  6170  inimass  6175  dminxp  6200  imainrect  6201  xpima  6202  rnresv  6221  imacnvcnv  6226  rnpropg  6242  imadmres  6254  mptpreima  6258  rnmpt0f  6263  dmco  6274  resdif  6869  fpr  7174  rnmptc  7227  fliftfuns  7334  rnoprab  7538  rnmpo  7566  elrnmpores  7571  curry1  8129  curry2  8132  fparlem3  8139  fparlem4  8140  fsplitfpar  8143  qliftfuns  8844  xpassen  9106  sbthlem6  9128  pwfir  9355  hartogslem1  9582  rnttrcl  9762  rankwflemb  9833  fin23lem34  10386  axcc2lem  10476  axdc2lem  10488  fpwwe2lem12  10682  seqval  14053  0rest  17474  imasdsval2  17561  fulloppc  17969  oppchofcl  18305  oyoncl  18315  gsumwspan  18859  pmtrprfvalrn  19506  psgnsn  19538  psgnprfval2  19541  oppglsm  19660  efgredlemg  19760  efgredlemd  19762  fincygsubgodd  20132  pjdm  21727  pf1rcl  22353  mpfpf1  22355  pf1ind  22359  leordtvallem1  23218  leordtvallem2  23219  leordtval  23221  cnconst2  23291  ptcmplem1  24060  tgpconncomp  24121  fmucndlem  24300  fmucnd  24301  ucnextcn  24313  metustto  24566  metustexhalf  24569  metuust  24573  cfilucfil2  24574  metuel  24577  psmetutop  24580  restmetu  24583  metucn  24584  minveclem5  25467  minvec  25470  ovolgelb  25515  ovoliunlem1  25537  itg1addlem4  25734  itg2seq  25777  itg2i1fseq  25790  itg2cnlem1  25796  efifo  26589  logrn  26600  dfrelog  26607  dvrelog  26679  xrlimcnp  27011  iedgedg  29067  edgiedgb  29071  edg0iedg0  29072  uhgrvtxedgiedgb  29153  uspgrf1oedg  29190  usgrf1oedg  29224  usgredg3  29233  ushgredgedg  29246  ushgredgedgloop  29248  usgrexmpledg  29279  0grsubgr  29295  uhgrspan1  29320  usgredgffibi  29341  dfnbgr3  29355  nbupgrres  29381  usgrnbcnvfv  29382  edginwlk  29653  wlkiswwlks2lem4  29892  wlkiswwlks2lem5  29893  clwlkclwwlk  30021  ex-rn  30459  bafval  30623  cnnvba  30698  minveco  30903  abrexexd  32528  imadifxp  32614  elrgspn  33250  elrgspnsubrun  33253  lsmsnorb  33419  prsrn  33914  raddcn  33928  pl1cn  33954  esumrnmpt2  34069  sitgclbn  34345  lfuhgr  35123  mvtval  35505  elmsubrn  35533  dfon4  35894  ellines  36153  rnmptsn  37336  f1omptsnlem  37337  icoreresf  37353  ptrest  37626  ovoliunnfl  37669  voliunnfl  37671  rngoueqz  37947  rngonegmn1l  37948  rngonegmn1r  37949  rngoneglmul  37950  rngonegrmul  37951  zerdivemp1x  37954  isdrngo2  37965  rngokerinj  37982  iscrngo2  38004  idlnegcl  38029  1idl  38033  0rngo  38034  smprngopr  38059  prnc  38074  isfldidl  38075  isdmn3  38081  rncnvepres  38304  imaopab  42270  mzpmfp  42758  dmnonrel  43603  imanonrel  43606  cnvrcl0  43638  ntrrn  44135  modelaxreplem2  44996  modelaxreplem3  44997  rnresun  45185  disjinfi  45197  imassmpt  45269  supxrleubrnmptf  45462  elicores  45546  limsupvaluz  45723  limsupmnflem  45735  limsupvaluz2  45753  limsup10ex  45788  liminf10ex  45789  liminflelimsuplem  45790  ioodvbdlimc1lem1  45946  ioodvbdlimc1  45948  ioodvbdlimc2  45950  fourierdlem42  46164  ioorrnopn  46320  subsaliuncl  46373  sge0sn  46394  sge0split  46424  sge0fodjrnlem  46431  sge0xaddlem2  46449  volicorescl  46568  hoidmvlelem3  46612  vonioolem2  46696  smflimsuplem1  46835  smflimsuplem3  46837  smflimsup  46843  fcoreslem2  47076  dfclnbgr3  47813  isuspgrim0lem  47871  uspgrimprop  47873  usgrexmpl1edg  47983  usgrexmpl2edg  47988