Theorem rneqi 5927

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

Syntax hints:   = wceq 1570  ran crn 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-cnv 5669  df-dm 5671  df-rn 5672

This theorem is referenced by:  rnmpt  5947  resima  6014  resima2  6015  mptima  6074  ima0  6079  rnuni  6146  imaundi  6147  imaundir  6148  inimass  6152  dminxp  6178  imainrect  6179  xpima  6180  rnresv  6200  imadifssran  6202  imacnvcnv  6207  rnpropg  6223  imadmres  6235  mptpreima  6239  rnmpt0f  6244  dmco  6256  resdif  6842  fpr  7151  rnmptc  7205  fliftfuns  7312  rnoprab  7515  rnmpo  7543  elrnmpores  7548  curry1  8095  curry2  8098  fparlem3  8105  fparlem4  8106  fsplitfpar  8109  qliftfuns  8798  xpassen  9055  sbthlem6  9076  pwfir  9272  hartogslem1  9500  rnttrcl  9687  rankwflemb  9761  fin23lem34  10325  axcc2lem  10415  axdc2lem  10427  fpwwe2lem12  10622  seqval  14044  0rest  17477  imasdsval2  17565  fulloppc  17976  oppchofcl  18311  oyoncl  18321  gsumwspan  18900  pmtrprfvalrn  19553  psgnsn  19585  psgnprfval2  19588  oppglsm  19707  efgredlemg  19807  efgredlemd  19809  fincygsubgodd  20179  pjdm  21857  pf1rcl  22509  mpfpf1  22511  pf1ind  22515  leordtvallem1  23367  leordtvallem2  23368  leordtval  23370  cnconst2  23440  ptcmplem1  24209  tgpconncomp  24270  fmucndlem  24447  fmucnd  24448  ucnextcn  24460  metustto  24710  metustexhalf  24713  metuust  24717  cfilucfil2  24718  metuel  24721  psmetutop  24724  restmetu  24727  metucn  24728  minveclem5  25592  minvec  25595  ovolgelb  25639  ovoliunlem1  25661  itg1addlem4  25858  itg2seq  25901  itg2i1fseq  25914  itg2cnlem1  25920  efifo  26712  logrn  26723  dfrelog  26730  dvrelog  26802  xrlimcnp  27133  iedgedg  29400  edgiedgb  29404  edg0iedg0  29405  uhgrvtxedgiedgb  29486  uspgrf1oedg  29523  usgrf1oedg  29557  usgredg3  29566  ushgredgedg  29579  ushgredgedgloop  29581  usgrexmpledg  29612  0grsubgr  29628  uhgrspan1  29653  usgredgffibi  29674  dfnbgr3  29688  nbupgrres  29714  usgrnbcnvfv  29715  edginwlk  29984  wlkiswwlks2lem4  30221  wlkiswwlks2lem5  30222  clwlkclwwlk  30353  ex-rn  30791  bafval  30956  cnnvba  31031  minveco  31236  abrexexd  32855  imadifxp  32946  elrgspn  33566  elrgspnsubrun  33569  lsmsnorb  33704  prsrn  34305  raddcn  34319  pl1cn  34345  esumrnmpt2  34458  sitgclbn  34733  lfuhgr  35610  mvtval  35992  elmsubrn  36020  dfon4  36383  ellines  36644  rnmptsn  37981  f1omptsnlem  37982  icoreresf  37998  ptrest  38270  ovoliunnfl  38313  voliunnfl  38315  rngoueqz  38591  rngonegmn1l  38592  rngonegmn1r  38593  rngoneglmul  38594  rngonegrmul  38595  zerdivemp1x  38598  isdrngo2  38609  rngokerinj  38626  iscrngo2  38648  idlnegcl  38673  1idl  38677  0rngo  38678  smprngopr  38703  prnc  38718  isfldidl  38719  isdmn3  38725  rncnvepres  38958  rnqmap  39103  dfsuccl2  39119  imaopab  43002  mzpmfp  43478  dmnonrel  44316  imanonrel  44319  cnvrcl0  44351  ntrrn  44848  modelaxreplem2  45688  modelaxreplem3  45689  rnresun  45898  disjinfi  45910  imassmpt  45977  supxrleubrnmptf  46165  elicores  46249  limsupvaluz  46422  limsupmnflem  46434  limsupvaluz2  46452  limsup10ex  46487  liminf10ex  46488  liminflelimsuplem  46489  ioodvbdlimc1lem1  46645  ioodvbdlimc1  46647  ioodvbdlimc2  46649  fourierdlem42  46863  ioorrnopn  47019  subsaliuncl  47072  sge0sn  47093  sge0split  47123  sge0fodjrnlem  47130  sge0xaddlem2  47148  volicorescl  47267  hoidmvlelem3  47311  vonioolem2  47395  smflimsuplem1  47534  smflimsuplem3  47536  smflimsup  47542  fcoreslem2  47801  dfclnbgr3  48591  isuspgrim0lem  48658  upgrimtrlslem2  48670  usgrexmpl1edg  48789  usgrexmpl2edg  48794