Theorem rneqi 5950

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

Syntax hints:   = wceq 1536  ran crn 5689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-cnv 5696  df-dm 5698  df-rn 5699

This theorem is referenced by:  rnmpt  5970  resima  6034  resima2  6035  mptima  6091  ima0  6096  rnuni  6170  imaundi  6171  imaundir  6172  inimass  6176  dminxp  6201  imainrect  6202  xpima  6203  rnresv  6222  imacnvcnv  6227  rnpropg  6243  imadmres  6255  mptpreima  6259  rnmpt0f  6264  dmco  6275  resdif  6869  fpr  7173  rnmptc  7226  fliftfuns  7333  rnoprab  7536  rnmpo  7565  elrnmpores  7570  curry1  8127  curry2  8130  fparlem3  8137  fparlem4  8138  fsplitfpar  8141  qliftfuns  8842  xpassen  9104  sbthlem6  9126  pwfir  9352  hartogslem1  9579  rnttrcl  9759  rankwflemb  9830  fin23lem34  10383  axcc2lem  10473  axdc2lem  10485  fpwwe2lem12  10679  seqval  14049  0rest  17475  imasdsval2  17562  fulloppc  17975  oppchofcl  18316  oyoncl  18326  gsumwspan  18871  pmtrprfvalrn  19520  psgnsn  19552  psgnprfval2  19555  oppglsm  19674  efgredlemg  19774  efgredlemd  19776  fincygsubgodd  20146  pjdm  21744  pf1rcl  22368  mpfpf1  22370  pf1ind  22374  leordtvallem1  23233  leordtvallem2  23234  leordtval  23236  cnconst2  23306  ptcmplem1  24075  tgpconncomp  24136  fmucndlem  24315  fmucnd  24316  ucnextcn  24328  metustto  24581  metustexhalf  24584  metuust  24588  cfilucfil2  24589  metuel  24592  psmetutop  24595  restmetu  24598  metucn  24599  minveclem5  25480  minvec  25483  ovolgelb  25528  ovoliunlem1  25550  itg1addlem4  25747  itg1addlem4OLD  25748  itg2seq  25791  itg2i1fseq  25804  itg2cnlem1  25810  efifo  26603  logrn  26614  dfrelog  26621  dvrelog  26693  xrlimcnp  27025  iedgedg  29081  edgiedgb  29085  edg0iedg0  29086  uhgrvtxedgiedgb  29167  uspgrf1oedg  29204  usgrf1oedg  29238  usgredg3  29247  ushgredgedg  29260  ushgredgedgloop  29262  usgrexmpledg  29293  0grsubgr  29309  uhgrspan1  29334  usgredgffibi  29355  dfnbgr3  29369  nbupgrres  29395  usgrnbcnvfv  29396  edginwlk  29667  wlkiswwlks2lem4  29901  wlkiswwlks2lem5  29902  clwlkclwwlk  30030  ex-rn  30468  bafval  30632  cnnvba  30707  minveco  30912  abrexexd  32536  imadifxp  32620  elrgspn  33235  lsmsnorb  33398  prsrn  33875  raddcn  33889  pl1cn  33915  esumrnmpt2  34048  sitgclbn  34324  lfuhgr  35101  mvtval  35484  elmsubrn  35512  dfon4  35874  ellines  36133  rnmptsn  37317  f1omptsnlem  37318  icoreresf  37334  ptrest  37605  ovoliunnfl  37648  voliunnfl  37650  rngoueqz  37926  rngonegmn1l  37927  rngonegmn1r  37928  rngoneglmul  37929  rngonegrmul  37930  zerdivemp1x  37933  isdrngo2  37944  rngokerinj  37961  iscrngo2  37983  idlnegcl  38008  1idl  38012  0rngo  38013  smprngopr  38038  prnc  38053  isfldidl  38054  isdmn3  38060  rncnvepres  38284  imaopab  42248  mzpmfp  42734  dmnonrel  43579  imanonrel  43582  cnvrcl0  43614  ntrrn  44111  modelaxreplem2  44943  modelaxreplem3  44944  rnresun  45122  disjinfi  45134  imassmpt  45207  supxrleubrnmptf  45400  elicores  45485  limsupvaluz  45663  limsupmnflem  45675  limsupvaluz2  45693  limsup10ex  45728  liminf10ex  45729  liminflelimsuplem  45730  ioodvbdlimc1lem1  45886  ioodvbdlimc1  45888  ioodvbdlimc2  45890  fourierdlem42  46104  ioorrnopn  46260  subsaliuncl  46313  sge0sn  46334  sge0split  46364  sge0fodjrnlem  46371  sge0xaddlem2  46389  volicorescl  46508  hoidmvlelem3  46552  vonioolem2  46636  smflimsuplem1  46775  smflimsuplem3  46777  smflimsup  46783  fcoreslem2  47013  dfclnbgr3  47750  isuspgrim0lem  47808  uspgrimprop  47810  usgrexmpl1edg  47918  usgrexmpl2edg  47923