Theorem rneqd 5228

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

Hypothesis

Ref	Expression
rneqd.1	|- ( ph -> A = B )

Assertion

Ref	Expression
rneqd	|- ( ph -> ran A = ran B )

Proof of Theorem rneqd

Step	Hyp	Ref	Expression
1		rneqd.1	. 2 |- ( ph -> A = B )
2		rneq 5226	. 2 |- ( A = B -> ran A = ran B )
3	1, 2	syl 16	1 |- ( ph -> ran A = ran B )

Syntax hints:   -> wi 4   = wceq 1379   ran crn 5000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-cnv 5007  df-dm 5009  df-rn 5010

This theorem is referenced by:  resima2  5305  imaeq1  5330  imaeq2  5331  resiima  5349  rnxpid  5438  xpima  5447  funimacnv  5658  fnima  5697  elxp4  6725  elxp5  6726  2ndval  6784  fo2nd  6802  f2ndres  6804  curry1  6872  curry2  6875  oarec  7208  en1  7579  xpassen  7608  xpdom2  7609  sbthlem4  7627  fodomr  7665  dffi3  7887  marypha2lem4  7894  ordtypelem9  7947  dfac12lem1  8519  dfac12r  8522  fin23lem32  8720  fin23lem34  8722  fin23lem35  8723  fin23lem36  8724  fin23lem38  8725  fin23lem39  8726  fin23lem41  8728  itunitc  8797  ttukeylem3  8887  fpwwe2lem6  9009  fpwwe2lem9  9012  wunex2  9112  wuncval2  9121  gruima  9176  rpnnen1  11209  hashf1lem1  12466  limsupval  13256  xpnnenOLD  13800  vdwapfval  14344  vdwapval  14346  vdwmc  14351  vdwpc  14353  vdwlem6  14359  vdwlem8  14361  restval  14678  restid2  14682  prdsval  14706  prdsdsval  14729  prdsdsval2  14735  prdsdsval3  14736  imasval  14762  imasdsval  14766  isfull  15133  arwval  15224  gsumvalx  15815  conjsubg  16093  pmtrfrn  16279  psgnfval  16321  sylow1lem2  16415  sylow1lem4  16417  sylow1  16419  sylow2blem1  16436  sylow2b  16439  sylow3lem1  16443  sylow3lem2  16444  sylow3lem3  16445  sylow3lem5  16447  sylow3lem6  16448  sylow3  16449  lsmfval  16454  lsmvalx  16455  oppglsm  16458  subglsm  16487  lsmpropd  16491  efgval2  16538  efgi2  16539  efgtlen  16540  efgsdm  16544  efgsdmi  16546  efgsrel  16548  efgs1b  16550  efgsp1  16551  efgsres  16552  efgsfo  16553  efgrelexlemb  16564  frgpnabllem1  16668  iscyg  16673  iscyggen  16674  gsumxp  16795  gsumxpOLD  16797  dprdval  16825  dprdvalOLD  16827  ablfac2  16930  evlseu  17956  zncyg  18354  cygznlem2a  18373  frlmsplit2  18570  tgrest  19426  ordtval  19456  ordtbas2  19458  ordtcnv  19468  ordtrest  19469  ordtrest2  19471  ispnrm  19606  cmpfi  19674  txval  19800  xkoval  19823  ptval2  19837  ptpjopn  19848  xkoccn  19855  xkoptsub  19890  xkopt  19891  fmval  20179  fmf  20181  txflf  20242  cnextf  20301  subgntr  20340  opnsubg  20341  clsnsg  20343  snclseqg  20349  tsmsval2  20363  tsmsxplem1  20390  ustuqtoplem  20477  utopsnneiplem  20485  utopsnneip  20486  fmucndlem  20529  ressprdsds  20609  mopnval  20676  metuvalOLD  20787  metuval  20788  metdsval  21086  lebnumlem1  21196  lebnumlem3  21198  pi1xfrcnvlem  21291  pi1xfrcnv  21292  minveclem3b  21578  elovolmr  21622  ovolctb  21636  ovoliunlem3  21650  ovolshftlem1  21655  voliunlem3  21697  voliun  21699  volsup  21701  uniioombllem2  21727  uniioombllem3  21729  mbflimsup  21808  itg1climres  21856  itg2monolem1  21892  itg2i1fseq  21897  itg2cnlem1  21903  ellimc2  22016  dvivth  22146  dvne0  22147  lhop2  22151  lhop  22152  mdegfval  22195  dchrptlem2  23268  dchrpt  23270  tglnunirn  23663  tgisline  23721  perpln1  23795  perpln2  23796  isperp  23797  lmif  23828  islmib  23830  edgval  24015  edgopval  24016  edgss  24028  nbgraop  24099  nbgraopALT  24100  ex-ima  24840  subgornss  24984  efghgrp  25051  isrngo  25056  drngoi  25085  vcoprne  25148  bafval  25173  pj3i  26803  ofrn2  27153  ffsrn  27224  ordtprsval  27536  ordtprsuni  27537  ordtcnvNEW  27538  ordtrestNEW  27539  ordtrest2NEW  27541  qqhval  27591  qqhval2  27599  esumval  27697  esumsn  27712  esumfsupre  27717  sxval  27801  omsval  27904  omsfval  27905  sibf0  27916  sitgfval  27923  cvmlift3lem6  28409  relexprn  28534  trpredeq1  28880  trpredeq2  28881  trpredeq3  28882  mblfinlem2  29629  ovoliunnfl  29633  voliunnfl  29635  filnetlem4  29802  rngohomval  29970  rngoisoval  29983  idlval  30013  pridlval  30033  maxidlval  30039  igenval  30061  mzpmfp  30283  mzpmfpOLD  30284  eldiophb  30294  diophrw  30296  fourierdlem60  31467  fourierdlem61  31468  fnrnafv  31714  csbima12gALTOLD  32702  lsatset  33787  docaffvalN  35918  docafvalN  35919  conrel1d  36781