Theorem rneqi 5220

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

Syntax hints:   = wceq 1374   ran crn 4993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-br 4441  df-opab 4499  df-cnv 5000  df-dm 5002  df-rn 5003

This theorem is referenced by:  rnmpt  5239  resima  5297  resima2  5298  ima0  5343  rnuni  5408  imaundi  5409  imaundir  5410  inimass  5413  dminxp  5438  imainrect  5439  xpima  5440  rnresv  5457  imacnvcnv  5463  rnpropg  5479  imadmres  5490  mptpreima  5491  dmco  5506  resdif  5827  fpr  6060  fliftfuns  6191  rnoprab  6360  rnmpt2  6387  elrnmpt2res  6391  curry1  6865  curry2  6868  fparlem3  6875  fparlem4  6876  qliftfuns  7388  xpassen  7601  sbthlem6  7622  dfsup3OLD  7893  hartogslem1  7956  rankwflemb  8200  fin23lem34  8715  axcc2lem  8805  axdc2lem  8817  fpwwe2lem13  9009  seqval  12074  0rest  14674  imasdsval2  14760  fulloppc  15138  oppchofcl  15376  oyoncl  15386  gsumwspan  15830  pmtrprfvalrn  16302  psgnsn  16334  psgnprfval2  16337  oppglsm  16451  efgredlemg  16549  efgredlemd  16551  dprdvalOLD  16820  pf1rcl  18149  mpfpf1  18151  pf1ind  18155  pjdm  18498  leordtvallem1  19470  leordtvallem2  19471  leordtval  19473  cnconst2  19543  ptcmplem1  20280  tgpconcomp  20339  fmucndlem  20522  fmucnd  20523  ucnextcn  20535  metusttoOLD  20788  metustto  20789  metustexhalfOLD  20794  metustexhalf  20795  metuustOLD  20802  metuust  20803  cfilucfil2OLD  20804  cfilucfil2  20805  metuelOLD  20808  metuel  20809  metutopOLD  20813  psmetutop  20814  restmetu  20818  metucnOLD  20819  metucn  20820  minveclem5  21576  minvec  21579  ovolgelb  21619  ovoliunlem1  21641  itg1addlem4  21834  itg2seq  21877  itg2i1fseq  21890  itg2cnlem1  21896  efifo  22660  logrn  22667  dfrelog  22674  dvrelog  22739  xrlimcnp  23019  usgrares1  24072  cusgrares  24134  ex-rn  24824  rngoueqz  25094  zerdivemp1  25098  rngoridfz  25099  bafval  25159  cnnvba  25246  minveco  25462  abrexexd  27067  imadifxp  27117  prsrn  27519  raddcn  27533  pl1cn  27559  sitgclbn  27911  ghomsn  28489  dfon4  29106  ellines  29365  ptrest  29612  ovoliunnfl  29620  voliunnfl  29622  rngonegmn1l  29942  rngonegmn1r  29943  rngoneglmul  29944  rngonegrmul  29945  zerdivemp1x  29948  isdrngo2  29951  rngokerinj  29968  iscrngo2  29985  idlnegcl  30009  1idl  30013  0rngo  30014  smprngopr  30039  prnc  30054  isfldidl  30055  isdmn3  30061  mzpmfp  30270  mzpmfpOLD  30271  ioodvbdlimc1lem1  31216  ioodvbdlimc1  31218  ioodvbdlimc2  31220  fourierdlem42  31404  fourierdlem45  31407  usgra2adedglem1  31780