Theorem rneqi 5913

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

Syntax hints:   = wceq 1560  ran crn 5648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-cnv 5655  df-dm 5657  df-rn 5658

This theorem is referenced by:  rnmpt  5933  resima  6001  resima2  6002  mptima  6061  ima0  6066  rnuni  6133  imaundi  6134  imaundir  6135  inimass  6140  dminxp  6166  imainrect  6167  xpima  6168  rnresv  6188  imacnvcnv  6193  rnpropg  6209  imadmres  6221  mptpreima  6225  rnmpt0f  6230  dmco  6242  resdif  6828  fpr  7137  rnmptc  7191  fliftfuns  7298  rnoprab  7501  rnmpo  7529  elrnmpores  7534  curry1  8083  curry2  8086  fparlem3  8093  fparlem4  8094  fsplitfpar  8097  qliftfuns  8786  xpassen  9043  sbthlem6  9064  pwfir  9261  hartogslem1  9490  rnttrcl  9677  rankwflemb  9751  fin23lem34  10303  axcc2lem  10393  axdc2lem  10405  fpwwe2lem12  10600  seqval  14025  0rest  17458  imasdsval2  17546  fulloppc  17957  oppchofcl  18292  oyoncl  18302  gsumwspan  18880  pmtrprfvalrn  19528  psgnsn  19560  psgnprfval2  19563  oppglsm  19682  efgredlemg  19782  efgredlemd  19784  fincygsubgodd  20154  pjdm  21759  pf1rcl  22412  mpfpf1  22414  pf1ind  22418  leordtvallem1  23270  leordtvallem2  23271  leordtval  23273  cnconst2  23343  ptcmplem1  24112  tgpconncomp  24173  fmucndlem  24350  fmucnd  24351  ucnextcn  24363  metustto  24613  metustexhalf  24616  metuust  24620  cfilucfil2  24621  metuel  24624  psmetutop  24627  restmetu  24630  metucn  24631  minveclem5  25495  minvec  25498  ovolgelb  25542  ovoliunlem1  25564  itg1addlem4  25761  itg2seq  25804  itg2i1fseq  25817  itg2cnlem1  25823  efifo  26612  logrn  26623  dfrelog  26630  dvrelog  26702  xrlimcnp  27033  iedgedg  29251  edgiedgb  29255  edg0iedg0  29256  uhgrvtxedgiedgb  29337  uspgrf1oedg  29374  usgrf1oedg  29408  usgredg3  29417  ushgredgedg  29430  ushgredgedgloop  29432  usgrexmpledg  29463  0grsubgr  29479  uhgrspan1  29504  usgredgffibi  29525  dfnbgr3  29539  nbupgrres  29565  usgrnbcnvfv  29566  edginwlk  29835  wlkiswwlks2lem4  30072  wlkiswwlks2lem5  30073  clwlkclwwlk  30204  ex-rn  30642  bafval  30807  cnnvba  30882  minveco  31087  abrexexd  32708  imadifxp  32801  elrgspn  33427  elrgspnsubrun  33430  lsmsnorb  33577  prsrn  34212  raddcn  34226  pl1cn  34252  esumrnmpt2  34365  sitgclbn  34640  lfuhgr  35468  mvtval  35850  elmsubrn  35878  dfon4  36241  ellines  36502  rnmptsn  37829  f1omptsnlem  37830  icoreresf  37846  ptrest  38118  ovoliunnfl  38161  voliunnfl  38163  rngoueqz  38439  rngonegmn1l  38440  rngonegmn1r  38441  rngoneglmul  38442  rngonegrmul  38443  zerdivemp1x  38446  isdrngo2  38457  rngokerinj  38474  iscrngo2  38496  idlnegcl  38521  1idl  38525  0rngo  38526  smprngopr  38551  prnc  38566  isfldidl  38567  isdmn3  38573  rncnvepres  38808  rnqmap  38953  dfsuccl2  38969  imaopab  42850  mzpmfp  43328  dmnonrel  44166  imanonrel  44169  cnvrcl0  44201  ntrrn  44698  modelaxreplem2  45555  modelaxreplem3  45556  rnresun  45758  disjinfi  45770  imassmpt  45837  supxrleubrnmptf  46025  elicores  46109  limsupvaluz  46282  limsupmnflem  46294  limsupvaluz2  46312  limsup10ex  46347  liminf10ex  46348  liminflelimsuplem  46349  ioodvbdlimc1lem1  46505  ioodvbdlimc1  46507  ioodvbdlimc2  46509  fourierdlem42  46723  ioorrnopn  46879  subsaliuncl  46932  sge0sn  46953  sge0split  46983  sge0fodjrnlem  46990  sge0xaddlem2  47008  volicorescl  47127  hoidmvlelem3  47171  vonioolem2  47255  smflimsuplem1  47394  smflimsuplem3  47396  smflimsup  47402  fcoreslem2  47658  dfclnbgr3  48448  isuspgrim0lem  48515  upgrimtrlslem2  48527  usgrexmpl1edg  48646  usgrexmpl2edg  48651