Theorem rneqd 5072

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 5070	. 2 |- ( A = B -> ran A = ran B )
3	1, 2	syl 16	1 |- ( ph -> ran A = ran B )

Syntax hints:   -> wi 4   = wceq 1369   ran crn 4846

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 2423

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 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-br 4298  df-opab 4356  df-cnv 4853  df-dm 4855  df-rn 4856

This theorem is referenced by:  resima2  5148  imaeq1  5169  imaeq2  5170  resiima  5188  rnxpid  5276  xpima  5285  funimacnv  5495  fnima  5534  elxp4  6527  elxp5  6528  2ndval  6585  fo2nd  6602  f2ndres  6604  curry1  6669  curry2  6672  oarec  7006  en1  7381  xpassen  7410  xpdom2  7411  sbthlem4  7429  fodomr  7467  dffi3  7686  marypha2lem4  7693  ordtypelem9  7745  dfac12lem1  8317  dfac12r  8320  fin23lem32  8518  fin23lem34  8520  fin23lem35  8521  fin23lem36  8522  fin23lem38  8523  fin23lem39  8524  fin23lem41  8526  itunitc  8595  ttukeylem3  8685  fpwwe2lem6  8807  fpwwe2lem9  8810  wunex2  8910  wuncval2  8919  gruima  8974  rpnnen1  10989  hashf1lem1  12213  limsupval  12957  xpnnenOLD  13497  vdwapfval  14037  vdwapval  14039  vdwmc  14044  vdwpc  14046  vdwlem6  14052  vdwlem8  14054  restval  14370  restid2  14374  prdsval  14398  prdsdsval  14421  prdsdsval2  14427  prdsdsval3  14428  imasval  14454  imasdsval  14458  isfull  14825  arwval  14916  gsumvalx  15507  conjsubg  15783  pmtrfrn  15969  psgnfval  16011  sylow1lem2  16103  sylow1lem4  16105  sylow1  16107  sylow2blem1  16124  sylow2b  16127  sylow3lem1  16131  sylow3lem2  16132  sylow3lem3  16133  sylow3lem5  16135  sylow3lem6  16136  sylow3  16137  lsmfval  16142  lsmvalx  16143  oppglsm  16146  subglsm  16175  lsmpropd  16179  efgval2  16226  efgi2  16227  efgtlen  16228  efgsdm  16232  efgsdmi  16234  efgsrel  16236  efgs1b  16238  efgsp1  16239  efgsres  16240  efgsfo  16241  efgrelexlemb  16252  frgpnabllem1  16356  iscyg  16361  iscyggen  16362  gsumxp  16473  gsumxpOLD  16475  dprdval  16490  dprdvalOLD  16492  ablfac2  16595  evlseu  17607  zncyg  17986  cygznlem2a  18005  frlmsplit2  18202  tgrest  18768  ordtval  18798  ordtbas2  18800  ordtcnv  18810  ordtrest  18811  ordtrest2  18813  ispnrm  18948  cmpfi  19016  txval  19142  xkoval  19165  ptval2  19179  ptpjopn  19190  xkoccn  19197  xkoptsub  19232  xkopt  19233  fmval  19521  fmf  19523  txflf  19584  cnextf  19643  subgntr  19682  opnsubg  19683  clsnsg  19685  snclseqg  19691  tsmsval2  19705  tsmsxplem1  19732  ustuqtoplem  19819  utopsnneiplem  19827  utopsnneip  19828  fmucndlem  19871  ressprdsds  19951  mopnval  20018  metuvalOLD  20129  metuval  20130  metdsval  20428  lebnumlem1  20538  lebnumlem3  20540  pi1xfrcnvlem  20633  pi1xfrcnv  20634  minveclem3b  20920  elovolmr  20964  ovolctb  20978  ovoliunlem3  20992  ovolshftlem1  20997  voliunlem3  21038  voliun  21040  volsup  21042  uniioombllem2  21068  uniioombllem3  21070  mbflimsup  21149  itg1climres  21197  itg2monolem1  21233  itg2i1fseq  21238  itg2cnlem1  21244  ellimc2  21357  dvivth  21487  dvne0  21488  lhop2  21492  lhop  21493  mdegfval  21536  dchrptlem2  22609  dchrpt  22611  tglnunirn  22987  tgisline  23039  isperp  23108  nbgraop  23340  ex-ima  23654  subgornss  23798  efghgrp  23865  isrngo  23870  drngoi  23899  vcoprne  23962  bafval  23987  pj3i  25617  ofrn2  25963  ffsrn  26034  ordtprsval  26353  ordtprsuni  26354  ordtcnvNEW  26355  ordtrestNEW  26356  ordtrest2NEW  26358  qqhval  26408  qqhval2  26416  esumval  26505  esumsn  26520  esumfsupre  26525  sxval  26609  omsval  26713  omsfval  26714  sibf0  26725  sitgfval  26732  cvmlift3lem6  27218  relexprn  27343  trpredeq1  27689  trpredeq2  27690  trpredeq3  27691  mblfinlem2  28434  ovoliunnfl  28438  voliunnfl  28440  filnetlem4  28607  rngohomval  28775  rngoisoval  28788  idlval  28818  pridlval  28838  maxidlval  28844  igenval  28866  mzpmfp  29088  mzpmfpOLD  29089  eldiophb  29100  diophrw  29102  fnrnafv  30073  csbima12gALTOLD  31563  lsatset  32640  docaffvalN  34771  docafvalN  34772