Theorem rneqi 5159

Description: Equality inference for range. (Contributed by NM, 4-Mar-2004.)

Hypothesis

Ref	Expression
rneqi.1	|- A = B

Assertion

Ref	Expression
rneqi	|- ran A = ran B

Proof of Theorem rneqi

Step	Hyp	Ref	Expression
1		rneqi.1	. 2 |- A = B
2		rneq 5158	. 2 |- ( A = B -> ran A = ran B )
3	1, 2	ax-mp 5	1 |- ran A = ran B

Syntax hints:   = wceq 1399   ran crn 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-rab 2755  df-v 3053  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3729  df-if 3875  df-sn 3962  df-pr 3964  df-op 3968  df-br 4385  df-opab 4443  df-cnv 4938  df-dm 4940  df-rn 4941

This theorem is referenced by:  rnmpt  5178  resima  5235  resima2  5236  ima0  5281  rnuni  5344  imaundi  5345  imaundir  5346  inimass  5349  dminxp  5374  imainrect  5375  xpima  5376  rnresv  5392  imacnvcnv  5397  rnpropg  5413  imadmres  5424  mptpreima  5425  dmco  5440  resdif  5761  fpr  5999  fliftfuns  6135  rnoprab  6306  rnmpt2  6333  elrnmpt2res  6337  curry1  6813  curry2  6816  fparlem3  6823  fparlem4  6824  qliftfuns  7338  xpassen  7552  sbthlem6  7573  hartogslem1  7904  rankwflemb  8146  fin23lem34  8661  axcc2lem  8751  axdc2lem  8763  fpwwe2lem13  8953  seqval  12044  0rest  14860  imasdsval2  14946  fulloppc  15351  oppchofcl  15669  oyoncl  15679  gsumwspan  16154  pmtrprfvalrn  16653  psgnsn  16685  psgnprfval2  16688  oppglsm  16802  efgredlemg  16900  efgredlemd  16902  dprdvalOLD  17172  pf1rcl  18521  mpfpf1  18523  pf1ind  18527  pjdm  18852  leordtvallem1  19820  leordtvallem2  19821  leordtval  19823  cnconst2  19893  ptcmplem1  20660  tgpconcomp  20719  fmucndlem  20902  fmucnd  20903  ucnextcn  20915  metusttoOLD  21168  metustto  21169  metustexhalfOLD  21174  metustexhalf  21175  metuustOLD  21182  metuust  21183  cfilucfil2OLD  21184  cfilucfil2  21185  metuelOLD  21188  metuel  21189  metutopOLD  21193  psmetutop  21194  restmetu  21198  metucnOLD  21199  metucn  21200  minveclem5  21956  minvec  21959  ovolgelb  21999  ovoliunlem1  22021  itg1addlem4  22214  itg2seq  22257  itg2i1fseq  22270  itg2cnlem1  22276  efifo  23042  logrn  23054  dfrelog  23061  dvrelog  23128  xrlimcnp  23438  usgrares1  24556  cusgrares  24618  ex-rn  25307  rngoueqz  25574  zerdivemp1  25578  rngoridfz  25579  bafval  25639  cnnvba  25726  minveco  25942  abrexexd  27552  imadifxp  27625  prsrn  28086  raddcn  28100  pl1cn  28126  esumrnmpt2  28251  sitgclbn  28508  mvtval  29089  elmsubrn  29117  ghomsn  29257  dfon4  29736  ellines  29995  ptrest  30253  ovoliunnfl  30261  voliunnfl  30263  rngonegmn1l  30558  rngonegmn1r  30559  rngoneglmul  30560  rngonegrmul  30561  zerdivemp1x  30564  isdrngo2  30567  rngokerinj  30584  iscrngo2  30601  idlnegcl  30625  1idl  30629  0rngo  30630  smprngopr  30655  prnc  30670  isfldidl  30671  isdmn3  30677  mzpmfp  30885  ioodvbdlimc1lem1  31933  ioodvbdlimc1  31935  ioodvbdlimc2  31937  fourierdlem42  32136  usgra2adedglem1  32713