Theorem rneqd 5056

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

Syntax hints:   -> wi 4   = wceq 1649   ran crn 4838

This theorem is referenced by:  resima2  5138  imaeq1  5157  imaeq2  5158  csbima12gALT  5173  resiima  5179  rnxpid  5261  xpima  5272  elxp4  5316  elxp5  5317  funimacnv  5484  fnima  5522  2ndval  6311  fo2nd  6326  f2ndres  6328  curry1  6397  curry2  6400  oarec  6764  en1  7133  xpassen  7161  xpdom2  7162  sbthlem4  7179  fodomr  7217  dffi3  7394  marypha2lem4  7401  ordtypelem9  7451  dfac12lem1  7979  dfac12r  7982  fin23lem32  8180  fin23lem34  8182  fin23lem35  8183  fin23lem36  8184  fin23lem38  8185  fin23lem39  8186  fin23lem41  8188  itunitc  8257  ttukeylem3  8347  fpwwe2lem6  8466  fpwwe2lem9  8469  wunex2  8569  wuncval2  8578  gruima  8633  rpnnen1  10561  hashf1lem1  11659  limsupval  12223  xpnnenOLD  12764  vdwapfval  13294  vdwapval  13296  vdwmc  13301  vdwpc  13303  vdwlem6  13309  vdwlem8  13311  restval  13609  restid2  13613  prdsval  13633  prdsdsval  13655  prdsdsval2  13661  prdsdsval3  13662  imasval  13692  imasdsval  13696  isfull  14062  arwval  14153  gsumvalx  14729  conjsubg  14992  sylow1lem2  15188  sylow1lem4  15190  sylow1  15192  sylow2blem1  15209  sylow2b  15212  sylow3lem1  15216  sylow3lem2  15217  sylow3lem3  15218  sylow3lem5  15220  sylow3lem6  15221  sylow3  15222  lsmfval  15227  lsmvalx  15228  oppglsm  15231  subglsm  15260  lsmpropd  15264  efgval2  15311  efgi2  15312  efgtlen  15313  efgsdm  15317  efgsdmi  15319  efgsrel  15321  efgs1b  15323  efgsp1  15324  efgsres  15325  efgsfo  15326  efgrelexlemb  15337  frgpnabllem1  15439  iscyg  15444  iscyggen  15445  gsumxp  15505  dprdval  15516  ablfac2  15602  zncyg  16784  cygznlem2a  16803  tgrest  17177  ordtval  17207  ordtbas2  17209  ordtcnv  17219  ordtrest  17220  ordtrest2  17222  ispnrm  17357  cmpfi  17425  txval  17549  xkoval  17572  ptval2  17586  ptpjopn  17597  xkoccn  17604  xkoptsub  17639  xkopt  17640  fmval  17928  fmf  17930  txflf  17991  cnextf  18050  subgntr  18089  opnsubg  18090  clsnsg  18092  snclseqg  18098  tsmsval2  18112  tsmsxplem1  18135  ustuqtoplem  18222  utopsnneiplem  18230  utopsnneip  18231  fmucndlem  18274  ressprdsds  18354  mopnval  18421  metuvalOLD  18532  metuval  18533  metdsval  18830  lebnumlem1  18939  lebnumlem3  18941  pi1xfrcnvlem  19034  pi1xfrcnv  19035  minveclem3b  19282  elovolmr  19325  ovolctb  19339  ovoliunlem3  19353  ovolshftlem1  19358  voliunlem3  19399  voliun  19401  volsup  19403  uniioombllem2  19428  uniioombllem3  19430  mbflimsup  19511  itg1climres  19559  itg2monolem1  19595  itg2i1fseq  19600  itg2cnlem1  19606  ellimc2  19717  dvivth  19847  dvne0  19848  lhop2  19852  lhop  19853  evlseu  19890  mdegfval  19938  dchrptlem2  21002  dchrpt  21004  nbgraop  21389  ex-ima  21703  subgornss  21847  efghgrp  21914  isrngo  21919  drngoi  21948  vcoprne  22011  bafval  22036  pj3i  23664  ofrn2  24006  qqhval  24311  qqhval2  24319  esumval  24394  esumsn  24409  esumfsupre  24414  sxval  24497  sibf0  24602  sitgfval  24608  cvmlift3lem6  24964  relexprn  25089  trpredeq1  25437  trpredeq2  25438  trpredeq3  25439  mblfinlem  26143  ovoliunnfl  26147  voliunnfl  26149  filnetlem4  26300  rngohomval  26470  rngoisoval  26483  idlval  26513  pridlval  26533  maxidlval  26539  igenval  26561  mzpmfp  26694  eldiophb  26705  diophrw  26707  frlmsplit2  27111  pmtrfrn  27268  psgnfval  27291  fnrnafv  27893  lsatset  29473  docaffvalN  31604  docafvalN  31605

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-cnv 4845  df-dm 4847  df-rn 4848