Theorem rneqi 5215

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

Syntax hints:   = wceq 1381   ran crn 4986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-br 4434  df-opab 4492  df-cnv 4993  df-dm 4995  df-rn 4996

This theorem is referenced by:  rnmpt  5234  resima  5292  resima2  5293  ima0  5338  rnuni  5403  imaundi  5404  imaundir  5405  inimass  5408  dminxp  5433  imainrect  5434  xpima  5435  rnresv  5452  imacnvcnv  5458  rnpropg  5474  imadmres  5485  mptpreima  5486  dmco  5501  resdif  5822  fpr  6060  fliftfuns  6193  rnoprab  6366  rnmpt2  6393  elrnmpt2res  6397  curry1  6873  curry2  6876  fparlem3  6883  fparlem4  6884  qliftfuns  7396  xpassen  7609  sbthlem6  7630  dfsup3OLD  7902  hartogslem1  7965  rankwflemb  8209  fin23lem34  8724  axcc2lem  8814  axdc2lem  8826  fpwwe2lem13  9018  seqval  12092  0rest  14699  imasdsval2  14785  fulloppc  15160  oppchofcl  15398  oyoncl  15408  gsumwspan  15883  pmtrprfvalrn  16382  psgnsn  16414  psgnprfval2  16417  oppglsm  16531  efgredlemg  16629  efgredlemd  16631  dprdvalOLD  16905  pf1rcl  18253  mpfpf1  18255  pf1ind  18259  pjdm  18605  leordtvallem1  19577  leordtvallem2  19578  leordtval  19580  cnconst2  19650  ptcmplem1  20418  tgpconcomp  20477  fmucndlem  20660  fmucnd  20661  ucnextcn  20673  metusttoOLD  20926  metustto  20927  metustexhalfOLD  20932  metustexhalf  20933  metuustOLD  20940  metuust  20941  cfilucfil2OLD  20942  cfilucfil2  20943  metuelOLD  20946  metuel  20947  metutopOLD  20951  psmetutop  20952  restmetu  20956  metucnOLD  20957  metucn  20958  minveclem5  21714  minvec  21717  ovolgelb  21757  ovoliunlem1  21779  itg1addlem4  21972  itg2seq  22015  itg2i1fseq  22028  itg2cnlem1  22034  efifo  22799  logrn  22811  dfrelog  22818  dvrelog  22883  xrlimcnp  23163  usgrares1  24275  cusgrares  24337  ex-rn  25026  rngoueqz  25297  zerdivemp1  25301  rngoridfz  25302  bafval  25362  cnnvba  25449  minveco  25665  abrexexd  27272  imadifxp  27323  prsrn  27763  raddcn  27777  pl1cn  27803  sitgclbn  28151  mvtval  28726  elmsubrn  28754  ghomsn  28894  dfon4  29511  ellines  29770  ptrest  30016  ovoliunnfl  30024  voliunnfl  30026  rngonegmn1l  30320  rngonegmn1r  30321  rngoneglmul  30322  rngonegrmul  30323  zerdivemp1x  30326  isdrngo2  30329  rngokerinj  30346  iscrngo2  30363  idlnegcl  30387  1idl  30391  0rngo  30392  smprngopr  30417  prnc  30432  isfldidl  30433  isdmn3  30439  mzpmfp  30647  mzpmfpOLD  30648  ioodvbdlimc1lem1  31628  ioodvbdlimc1  31630  ioodvbdlimc2  31632  fourierdlem42  31816  usgra2adedglem1  32190