Theorem rneqi 5925

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

This proof depends on syntax axioms:   = wceq 1570  ran crn 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is used by:  rnmpt  5945  resima  6012  resima2  6013  mptima  6072  ima0  6077  rnuni  6144  imaundi  6145  imaundir  6146  inimass  6150  dminxp  6177  imainrect  6178  xpima  6179  rnresv  6199  imadifssran  6201  imacnvcnv  6206  rnpropg  6222  imadmres  6234  mptpreima  6238  rnmpt0f  6243  dmco  6255  resdif  6843  fpr  7155  rnmptc  7210  fliftfuns  7319  rnoprab  7522  rnmpo  7550  elrnmpores  7555  curry1  8105  curry2  8108  fparlem3  8115  fparlem4  8116  fsplitfpar  8119  qliftfuns  8808  xpassen  9073  sbthlem6  9094  pwfir  9290  hartogslem1  9518  rnttrcl  9705  rankwflemb  9779  fin23lem34  10352  axcc2lem  10442  axdc2lem  10454  fpwwe2lem12  10655  seqval  14080  0rest  17520  imasdsval2  17608  fulloppc  18019  oppchofcl  18354  oyoncl  18364  gsumwspan  18961  pmtrprfvalrn  19621  psgnsn  19653  psgnprfval2  19656  oppglsm  19775  efgredlemg  19875  efgredlemd  19877  fincygsubgodd  20247  pjdm  21926  pf1rcl  22580  mpfpf1  22582  pf1ind  22586  leordtvallem1  23441  leordtvallem2  23442  leordtval  23444  cnconst2  23514  ptcmplem1  24284  tgpconncomp  24345  fmucndlem  24522  fmucnd  24523  ucnextcn  24535  metustto  24785  metustexhalf  24788  metuust  24792  cfilucfil2  24793  metuel  24796  psmetutop  24799  restmetu  24802  metucn  24803  minveclem5  25667  minvec  25670  ovolgelb  25714  ovoliunlem1  25736  itg1addlem4  25933  itg2seq  25976  itg2i1fseq  25989  itg2cnlem1  25995  efifo  26792  logrn  26803  dfrelog  26810  dvrelog  26882  xrlimcnp  27213  iedgedg  29515  edgiedgb  29519  edg0iedg0  29520  uhgrvtxedgiedgb  29601  lfuhgr  29613  uspgrf1oedg  29641  usgrf1oedg  29675  usgredg3  29684  ushgredgedg  29697  ushgredgedgloop  29699  usgrexmpledg  29730  0grsubgr  29746  uhgrspan1  29771  usgredgffibi  29792  dfnbgr3  29806  nbupgrres  29832  usgrnbcnvfv  29833  edginwlk  30102  wlkiswwlks2lem4  30348  wlkiswwlks2lem5  30349  clwlkclwwlk  30480  ex-rn  30928  bafval  31093  cnnvba  31168  minveco  31373  abrexexd  32992  imadifxp  33082  elrgspn  33694  elrgspnsubrun  33697  lsmsnorb  33832  prsrn  34433  raddcn  34447  pl1cn  34473  esumrnmpt2  34586  sitgclbn  34862  mvtval  36087  elmsubrn  36115  dfon4  36478  ellines  36740  rnmptsn  38097  f1omptsnlem  38098  icoreresf  38114  ptrest  38376  ovoliunnfl  38419  voliunnfl  38421  rngoueqz  38698  rngonegmn1l  38699  rngonegmn1r  38700  rngoneglmul  38701  rngonegrmul  38702  zerdivemp1x  38705  isdrngo2  38716  rngokerinj  38733  iscrngo2  38755  idlnegcl  38780  1idl  38784  0rngo  38785  smprngopr  38810  prnc  38825  isfldidl  38826  isdmn3  38832  rncnvepres  39065  rnqmap  39210  dfsuccl2  39226  imaopab  43109  mzpmfp  43600  dmnonrel  44438  imanonrel  44441  cnvrcl0  44473  ntrrn  44970  modelaxreplem2  45810  modelaxreplem3  45811  rnresun  46020  disjinfi  46032  imassmpt  46099  supxrleubrnmptf  46287  elicores  46371  limsupvaluz  46544  limsupmnflem  46556  limsupvaluz2  46574  limsup10ex  46609  liminf10ex  46610  liminflelimsuplem  46611  ioodvbdlimc1lem1  46767  ioodvbdlimc1  46769  ioodvbdlimc2  46771  fourierdlem42  46985  ioorrnopn  47141  subsaliuncl  47194  sge0sn  47215  sge0split  47245  sge0fodjrnlem  47252  sge0xaddlem2  47270  volicorescl  47389  hoidmvlelem3  47433  vonioolem2  47517  smflimsuplem1  47656  smflimsuplem3  47658  smflimsup  47664  fcoreslem2  47960  dfclnbgr3  48750  isuspgrim0lem  48817  upgrimtrlslem2  48829  usgrexmpl1edg  48948  usgrexmpl2edg  48953