Theorem rneqi 5061

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

Syntax hints:   = wceq 1369   ran crn 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-br 4288  df-opab 4346  df-cnv 4843  df-dm 4845  df-rn 4846

This theorem is referenced by:  rnmpt  5080  resima  5137  resima2  5138  ima0  5179  rnuni  5243  imaundi  5244  imaundir  5245  inimass  5248  dminxp  5273  imainrect  5274  xpima  5275  rnresv  5292  imacnvcnv  5298  rnpropg  5314  imadmres  5325  mptpreima  5326  dmco  5341  resdif  5656  fpr  5885  fliftfuns  6002  rnoprab  6168  rnmpt2  6195  elrnmpt2res  6199  curry1  6659  curry2  6662  fparlem3  6669  fparlem4  6670  qliftfuns  7179  xpassen  7397  sbthlem6  7418  dfsup3OLD  7686  hartogslem1  7748  rankwflemb  7992  fin23lem34  8507  axcc2lem  8597  axdc2lem  8609  fpwwe2lem13  8801  seqval  11809  0rest  14360  imasdsval2  14446  fulloppc  14824  oppchofcl  15062  oyoncl  15072  gsumwspan  15515  pmtrprfvalrn  15985  psgnprfval2  16018  oppglsm  16132  efgredlemg  16230  efgredlemd  16232  dprdvalOLD  16475  pf1rcl  17758  mpfpf1  17760  pf1ind  17764  pjdm  18107  leordtvallem1  18789  leordtvallem2  18790  leordtval  18792  cnconst2  18862  ptcmplem1  19599  tgpconcomp  19658  fmucndlem  19841  fmucnd  19842  ucnextcn  19854  metusttoOLD  20107  metustto  20108  metustexhalfOLD  20113  metustexhalf  20114  metuustOLD  20121  metuust  20122  cfilucfil2OLD  20123  cfilucfil2  20124  metuelOLD  20127  metuel  20128  metutopOLD  20132  psmetutop  20133  restmetu  20137  metucnOLD  20138  metucn  20139  minveclem5  20895  minvec  20898  ovolgelb  20938  ovoliunlem1  20960  itg1addlem4  21152  itg2seq  21195  itg2i1fseq  21208  itg2cnlem1  21214  efifo  21978  logrn  21985  dfrelog  21992  dvrelog  22057  xrlimcnp  22337  usgrares1  23274  cusgrares  23331  ex-rn  23598  rngoueqz  23868  zerdivemp1  23872  rngoridfz  23873  bafval  23933  cnnvba  24020  minveco  24236  abrexexd  25841  imadifxp  25890  prsrn  26297  raddcn  26311  pl1cn  26337  sitgclbn  26681  ghomsn  27258  dfon4  27875  ellines  28134  ptrest  28378  ovoliunnfl  28386  voliunnfl  28388  rngonegmn1l  28708  rngonegmn1r  28709  rngoneglmul  28710  rngonegrmul  28711  zerdivemp1x  28714  isdrngo2  28717  rngokerinj  28734  iscrngo2  28751  idlnegcl  28775  1idl  28779  0rngo  28780  smprngopr  28805  prnc  28820  isfldidl  28821  isdmn3  28827  mzpmfp  29036  mzpmfpOLD  29037  usgra2adedglem1  30261  psgnsn  30722