Theorem rneqi 5920

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

This proof depends on syntax axioms:   = wceq 1569  ran crn 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-cnv 5659  df-dm 5661  df-rn 5662

This theorem is used by:  rnmpt  5940  resima  6058  resima2  6059  mptima  6072  ima0  6077  rnuni  6142  imaundi  6143  imaundir  6144  inimass  6147  dminxp  6174  imainrect  6175  xpima  6176  rnresv  6198  imadifssranOLD  6205  imacnvcnv  6210  rnpropg  6226  imadmres  6238  mptpreima  6242  rnmpt0f  6247  dmco  6259  resdif  6851  fpr  7163  rnmptc  7217  fliftfuns  7326  rnoprab  7529  rnmpo  7557  elrnmpores  7562  curry1  8122  curry2  8125  fparlem3  8132  fparlem4  8133  fsplitfpar  8136  qliftfuns  8833  xpassen  9098  sbthlem6  9119  pwfir  9316  hartogslem1  9543  rnttrcl  9730  rankwflembOLD  9808  fin23lem34  10431  axcc2lem  10521  axdc2lem  10533  fpwwe2lem12  10734  seqval  14162  0rest  17609  imasdsval2  17697  fulloppc  18108  oppchofcl  18443  oyoncl  18453  gsumwspan  19051  pmtrprfvalrn  19711  psgnsn  19743  psgnprfval2  19746  oppglsm  19865  efgredlemg  19965  efgredlemd  19967  fincygsubgodd  20337  pjdm  22022  pf1rcl  22676  mpfpf1  22678  pf1ind  22682  leordtvallem1  23537  leordtvallem2  23538  leordtval  23540  cnconst2  23610  ptcmplem1  24380  tgpconncomp  24441  fmucndlem  24618  fmucnd  24619  ucnextcn  24631  metustto  24881  metustexhalf  24884  metuust  24888  cfilucfil2  24889  metuel  24892  psmetutop  24895  restmetu  24898  metucn  24899  minveclem5  25763  minvec  25766  ovolgelb  25810  ovoliunlem1  25832  itg1addlem4  26029  itg2seq  26072  itg2i1fseq  26085  itg2cnlem1  26091  efifo  26884  logrn  26895  dfrelog  26902  dvrelog  26974  xrlimcnp  27305  iedgedg  29637  edgiedgb  29641  edg0iedg0  29642  uhgrvtxedgiedgb  29723  lfuhgr  29735  uspgrf1oedg  29763  usgrf1oedg  29797  usgredg3  29806  ushgredgedg  29819  ushgredgedgloop  29821  usgrexmpledg  29852  0grsubgr  29868  uhgrspan1  29893  usgredgffibi  29914  dfnbgr3  29928  nbupgrres  29954  usgrnbcnvfv  29955  edginwlk  30224  wlkiswwlks2lem4  30470  wlkiswwlks2lem5  30471  clwlkclwwlk  30602  ex-rn  31050  bafval  31215  cnnvba  31290  minveco  31495  abrexexd  33156  imadifxp  33246  elrgspn  33857  elrgspnsubrun  33860  lsmsnorb  33996  prsrn  34597  raddcn  34611  pl1cn  34637  esumrnmpt2  34750  sitgclbn  35025  mvtval  36383  elmsubrn  36411  dfon4  36779  ellines  37041  rnmptsn  38395  f1omptsnlem  38396  icoreresf  38412  ptrest  38674  ovoliunnfl  38717  voliunnfl  38719  rngoueqz  39011  rngonegmn1l  39012  rngonegmn1r  39013  rngoneglmul  39014  rngonegrmul  39015  zerdivemp1x  39018  isdrngo2  39029  rngokerinj  39046  iscrngo2  39068  idlnegcl  39093  1idl  39097  0rngo  39098  smprngopr  39123  prnc  39138  isfldidl  39139  isdmn3  39145  rncnvepres  39378  rnqmap  39523  dfsuccl2  39539  imaopab  43422  mzpmfp  43895  dmnonrel  44727  imanonrel  44730  cnvrcl0  44762  ntrrn  45259  modelaxreplem2  46105  modelaxreplem3  46106  rnresun  46331  disjinfi  46343  imassmpt  46410  supxrleubrnmptf  46597  elicores  46681  limsupvaluz  46854  limsupmnflem  46866  limsupvaluz2  46884  limsup10ex  46919  liminf10ex  46920  liminflelimsuplem  46921  ioodvbdlimc1lem1  47077  ioodvbdlimc1  47079  ioodvbdlimc2  47081  fourierdlem42  47295  ioorrnopn  47451  subsaliuncl  47504  sge0sn  47525  sge0split  47555  sge0fodjrnlem  47562  sge0xaddlem2  47580  volicorescl  47699  hoidmvlelem3  47743  vonioolem2  47827  smflimsuplem1  47966  smflimsuplem3  47968  smflimsup  47974  fcoreslem2  48270  dfclnbgr3  49060  isuspgrim0lem  49127  upgrimtrlslem2  49139  usgrexmpl1edg  49258  usgrexmpl2edg  49263