Theorem rneqi 5079

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 5078	. 2 |- ( A = B -> ran A = ran B )
3	1, 2	ax-mp 5	1 |- ran A = ran B

Syntax hints:   = wceq 1454   ran crn 4853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-br 4416  df-opab 4475  df-cnv 4860  df-dm 4862  df-rn 4863

This theorem is referenced by:  rnmpt  5098  resima  5155  resima2  5156  ima0  5201  rnuni  5265  imaundi  5266  imaundir  5267  inimass  5270  dminxp  5295  imainrect  5296  xpima  5297  rnresv  5313  imacnvcnv  5318  rnpropg  5334  imadmres  5345  mptpreima  5346  dmco  5361  resdif  5856  fpr  6095  fliftfuns  6231  rnoprab  6405  rnmpt2  6432  elrnmpt2res  6436  curry1  6914  curry2  6917  fparlem3  6924  fparlem4  6925  qliftfuns  7475  xpassen  7691  sbthlem6  7712  hartogslem1  8082  rankwflemb  8289  fin23lem34  8801  axcc2lem  8891  axdc2lem  8903  fpwwe2lem13  9092  seqval  12255  0rest  15376  imasdsval2  15465  imasdsval2OLD  15477  fulloppc  15875  oppchofcl  16193  oyoncl  16203  gsumwspan  16678  pmtrprfvalrn  17177  psgnsn  17209  psgnprfval2  17212  oppglsm  17342  efgredlemg  17440  efgredlemd  17442  pf1rcl  18985  mpfpf1  18987  pf1ind  18991  pjdm  19318  leordtvallem1  20274  leordtvallem2  20275  leordtval  20277  cnconst2  20347  ptcmplem1  21115  tgpconcomp  21175  fmucndlem  21354  fmucnd  21355  ucnextcn  21367  metustto  21616  metustexhalf  21619  metuust  21623  cfilucfil2  21624  metuel  21627  psmetutop  21630  restmetu  21633  metucn  21634  minveclem5  22423  minvec  22426  minveclem5OLD  22435  minvecOLD  22438  ovolgelb  22481  ovoliunlem1  22503  itg1addlem4  22705  itg2seq  22748  itg2i1fseq  22761  itg2cnlem1  22767  efifo  23544  logrn  23556  dfrelog  23563  dvrelog  23630  xrlimcnp  23942  usgrares1  25186  cusgrares  25248  ex-rn  25938  rngoueqz  26206  zerdivemp1  26210  rngoridfz  26211  bafval  26271  cnnvba  26358  minveco  26574  minvecoOLD  26584  abrexexd  28191  imadifxp  28260  prsrn  28769  raddcn  28783  pl1cn  28809  esumrnmpt2  28937  sitgclbn  29224  mvtval  30186  elmsubrn  30214  ghomsn  30354  dfon4  30708  ellines  30967  rnmptsn  31781  f1omptsnlem  31782  icoreresf  31799  ptrest  31983  ovoliunnfl  32026  voliunnfl  32028  rngonegmn1l  32232  rngonegmn1r  32233  rngoneglmul  32234  rngonegrmul  32235  zerdivemp1x  32238  isdrngo2  32241  rngokerinj  32258  iscrngo2  32275  idlnegcl  32299  1idl  32303  0rngo  32304  smprngopr  32329  prnc  32344  isfldidl  32345  isdmn3  32351  mzpmfp  35633  dmnonrel  36240  imanonrel  36243  cnvrcl0  36276  rnresun  37485  disjinfi  37505  elicores  37672  ioodvbdlimc1lem1  37840  ioodvbdlimc1lem1OLD  37842  ioodvbdlimc1  37844  ioodvbdlimc2  37847  fourierdlem42  38049  fourierdlem42OLD  38050  sge0sn  38258  sge0split  38288  sge0fodjrnlem  38295  sge0xaddlem2  38313  volicorescl  38412  hoidmvlelem3  38456  uhgrvtxedgiedgb  39274  uspgrf1oedg  39307  usgrf1oedg  39337  usgredg3  39342  ushgredgedga  39355  ushgredgedgaloop  39357  usgrexmpledg  39383  0grsubgr  39399  uhgrspan1  39424  usgredgffibi  39439  dfnbgr3  39457  nbupgrres  39487  usgrnbcnvfv  39488  edginwlk  39694  usgra2adedglem1  39942