Theorem rneqi 5879

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

Syntax hints:   = wceq 1540  ran crn 5620

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-cnv 5627  df-dm 5629  df-rn 5630

This theorem is referenced by:  rnmpt  5899  resima  5966  resima2  5967  mptima  6023  ima0  6028  rnuni  6097  imaundi  6098  imaundir  6099  inimass  6104  dminxp  6129  imainrect  6130  xpima  6131  rnresv  6150  imacnvcnv  6155  rnpropg  6171  imadmres  6183  mptpreima  6187  rnmpt0f  6192  dmco  6203  resdif  6785  fpr  7088  rnmptc  7143  fliftfuns  7251  rnoprab  7454  rnmpo  7482  elrnmpores  7487  curry1  8037  curry2  8040  fparlem3  8047  fparlem4  8048  fsplitfpar  8051  qliftfuns  8731  xpassen  8988  sbthlem6  9009  pwfir  9206  hartogslem1  9434  rnttrcl  9618  rankwflemb  9689  fin23lem34  10240  axcc2lem  10330  axdc2lem  10342  fpwwe2lem12  10536  seqval  13919  0rest  17333  imasdsval2  17420  fulloppc  17831  oppchofcl  18166  oyoncl  18176  gsumwspan  18720  pmtrprfvalrn  19367  psgnsn  19399  psgnprfval2  19402  oppglsm  19521  efgredlemg  19621  efgredlemd  19623  fincygsubgodd  19993  pjdm  21614  pf1rcl  22234  mpfpf1  22236  pf1ind  22240  leordtvallem1  23095  leordtvallem2  23096  leordtval  23098  cnconst2  23168  ptcmplem1  23937  tgpconncomp  23998  fmucndlem  24176  fmucnd  24177  ucnextcn  24189  metustto  24439  metustexhalf  24442  metuust  24446  cfilucfil2  24447  metuel  24450  psmetutop  24453  restmetu  24456  metucn  24457  minveclem5  25331  minvec  25334  ovolgelb  25379  ovoliunlem1  25401  itg1addlem4  25598  itg2seq  25641  itg2i1fseq  25654  itg2cnlem1  25660  efifo  26454  logrn  26465  dfrelog  26472  dvrelog  26544  xrlimcnp  26876  iedgedg  28995  edgiedgb  28999  edg0iedg0  29000  uhgrvtxedgiedgb  29081  uspgrf1oedg  29118  usgrf1oedg  29152  usgredg3  29161  ushgredgedg  29174  ushgredgedgloop  29176  usgrexmpledg  29207  0grsubgr  29223  uhgrspan1  29248  usgredgffibi  29269  dfnbgr3  29283  nbupgrres  29309  usgrnbcnvfv  29310  edginwlk  29580  wlkiswwlks2lem4  29817  wlkiswwlks2lem5  29818  clwlkclwwlk  29946  ex-rn  30384  bafval  30548  cnnvba  30623  minveco  30828  abrexexd  32453  imadifxp  32545  elrgspn  33186  elrgspnsubrun  33189  lsmsnorb  33328  prsrn  33882  raddcn  33896  pl1cn  33922  esumrnmpt2  34035  sitgclbn  34311  lfuhgr  35095  mvtval  35477  elmsubrn  35505  dfon4  35871  ellines  36130  rnmptsn  37313  f1omptsnlem  37314  icoreresf  37330  ptrest  37603  ovoliunnfl  37646  voliunnfl  37648  rngoueqz  37924  rngonegmn1l  37925  rngonegmn1r  37926  rngoneglmul  37927  rngonegrmul  37928  zerdivemp1x  37931  isdrngo2  37942  rngokerinj  37959  iscrngo2  37981  idlnegcl  38006  1idl  38010  0rngo  38011  smprngopr  38036  prnc  38051  isfldidl  38052  isdmn3  38058  rncnvepres  38281  imaopab  42208  mzpmfp  42724  dmnonrel  43567  imanonrel  43570  cnvrcl0  43602  ntrrn  44099  modelaxreplem2  44957  modelaxreplem3  44958  rnresun  45162  disjinfi  45174  imassmpt  45244  supxrleubrnmptf  45434  elicores  45518  limsupvaluz  45693  limsupmnflem  45705  limsupvaluz2  45723  limsup10ex  45758  liminf10ex  45759  liminflelimsuplem  45760  ioodvbdlimc1lem1  45916  ioodvbdlimc1  45918  ioodvbdlimc2  45920  fourierdlem42  46134  ioorrnopn  46290  subsaliuncl  46343  sge0sn  46364  sge0split  46394  sge0fodjrnlem  46401  sge0xaddlem2  46419  volicorescl  46538  hoidmvlelem3  46582  vonioolem2  46666  smflimsuplem1  46805  smflimsuplem3  46807  smflimsup  46813  fcoreslem2  47052  dfclnbgr3  47814  isuspgrim0lem  47881  upgrimtrlslem2  47893  usgrexmpl1edg  48012  usgrexmpl2edg  48017