Theorem rneqi 5934

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

Syntax hints:   = wceq 1541  ran crn 5676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-cnv 5683  df-dm 5685  df-rn 5686

This theorem is referenced by:  rnmpt  5952  resima  6013  resima2  6014  mptima  6069  ima0  6073  rnuni  6145  imaundi  6146  imaundir  6147  inimass  6151  dminxp  6176  imainrect  6177  xpima  6178  rnresv  6197  imacnvcnv  6202  rnpropg  6218  imadmres  6230  mptpreima  6234  rnmpt0f  6239  dmco  6250  resdif  6851  fpr  7148  rnmptc  7204  fliftfuns  7307  rnoprab  7508  rnmpo  7538  elrnmpores  7542  curry1  8086  curry2  8089  fparlem3  8096  fparlem4  8097  fsplitfpar  8100  qliftfuns  8794  xpassen  9062  sbthlem6  9084  pwfir  9172  hartogslem1  9533  rnttrcl  9713  rankwflemb  9784  fin23lem34  10337  axcc2lem  10427  axdc2lem  10439  fpwwe2lem12  10633  seqval  13973  0rest  17371  imasdsval2  17458  fulloppc  17869  oppchofcl  18209  oyoncl  18219  gsumwspan  18723  pmtrprfvalrn  19350  psgnsn  19382  psgnprfval2  19385  oppglsm  19504  efgredlemg  19604  efgredlemd  19606  fincygsubgodd  19976  pjdm  21253  pf1rcl  21859  mpfpf1  21861  pf1ind  21865  leordtvallem1  22705  leordtvallem2  22706  leordtval  22708  cnconst2  22778  ptcmplem1  23547  tgpconncomp  23608  fmucndlem  23787  fmucnd  23788  ucnextcn  23800  metustto  24053  metustexhalf  24056  metuust  24060  cfilucfil2  24061  metuel  24064  psmetutop  24067  restmetu  24070  metucn  24071  minveclem5  24941  minvec  24944  ovolgelb  24988  ovoliunlem1  25010  itg1addlem4  25207  itg1addlem4OLD  25208  itg2seq  25251  itg2i1fseq  25264  itg2cnlem1  25270  efifo  26047  logrn  26058  dfrelog  26065  dvrelog  26136  xrlimcnp  26462  iedgedg  28299  edgiedgb  28303  edg0iedg0  28304  uhgrvtxedgiedgb  28385  uspgrf1oedg  28422  usgrf1oedg  28453  usgredg3  28462  ushgredgedg  28475  ushgredgedgloop  28477  usgrexmpledg  28508  0grsubgr  28524  uhgrspan1  28549  usgredgffibi  28570  dfnbgr3  28584  nbupgrres  28610  usgrnbcnvfv  28611  edginwlk  28881  wlkiswwlks2lem4  29115  wlkiswwlks2lem5  29116  clwlkclwwlk  29244  ex-rn  29682  bafval  29844  cnnvba  29919  minveco  30124  abrexexd  31733  imadifxp  31819  lsmsnorb  32489  prsrn  32883  raddcn  32897  pl1cn  32923  esumrnmpt2  33054  sitgclbn  33330  lfuhgr  34096  mvtval  34479  elmsubrn  34507  dfon4  34853  ellines  35112  rnmptsn  36204  f1omptsnlem  36205  icoreresf  36221  ptrest  36475  ovoliunnfl  36518  voliunnfl  36520  rngoueqz  36796  rngonegmn1l  36797  rngonegmn1r  36798  rngoneglmul  36799  rngonegrmul  36800  zerdivemp1x  36803  isdrngo2  36814  rngokerinj  36831  iscrngo2  36853  idlnegcl  36878  1idl  36882  0rngo  36883  smprngopr  36908  prnc  36923  isfldidl  36924  isdmn3  36930  rncnvepres  37160  imaopab  41047  mzpmfp  41470  dmnonrel  42326  imanonrel  42329  cnvrcl0  42361  ntrrn  42858  rnresun  43861  disjinfi  43876  imassmpt  43953  supxrleubrnmptf  44147  elicores  44232  limsupvaluz  44410  limsupmnflem  44422  limsupvaluz2  44440  limsup10ex  44475  liminf10ex  44476  liminflelimsuplem  44477  ioodvbdlimc1lem1  44633  ioodvbdlimc1  44635  ioodvbdlimc2  44637  fourierdlem42  44851  ioorrnopn  45007  subsaliuncl  45060  sge0sn  45081  sge0split  45111  sge0fodjrnlem  45118  sge0xaddlem2  45136  volicorescl  45255  hoidmvlelem3  45299  vonioolem2  45383  smflimsuplem1  45522  smflimsuplem3  45524  smflimsup  45530  fcoreslem2  45760