Theorem rneqd 5054

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

Syntax hints:   -> wi 4   = wceq 1362   ran crn 4828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281  df-opab 4339  df-cnv 4835  df-dm 4837  df-rn 4838

This theorem is referenced by:  resima2  5131  imaeq1  5152  imaeq2  5153  resiima  5171  rnxpid  5259  xpima  5268  funimacnv  5478  fnima  5517  elxp4  6511  elxp5  6512  2ndval  6569  fo2nd  6586  f2ndres  6588  curry1  6653  curry2  6656  oarec  6989  en1  7364  xpassen  7393  xpdom2  7394  sbthlem4  7412  fodomr  7450  dffi3  7669  marypha2lem4  7676  ordtypelem9  7728  dfac12lem1  8300  dfac12r  8303  fin23lem32  8501  fin23lem34  8503  fin23lem35  8504  fin23lem36  8505  fin23lem38  8506  fin23lem39  8507  fin23lem41  8509  itunitc  8578  ttukeylem3  8668  fpwwe2lem6  8789  fpwwe2lem9  8792  wunex2  8892  wuncval2  8901  gruima  8956  rpnnen1  10971  hashf1lem1  12191  limsupval  12935  xpnnenOLD  13474  vdwapfval  14014  vdwapval  14016  vdwmc  14021  vdwpc  14023  vdwlem6  14029  vdwlem8  14031  restval  14347  restid2  14351  prdsval  14375  prdsdsval  14398  prdsdsval2  14404  prdsdsval3  14405  imasval  14431  imasdsval  14435  isfull  14802  arwval  14893  gsumvalx  15483  conjsubg  15757  pmtrfrn  15943  psgnfval  15985  sylow1lem2  16077  sylow1lem4  16079  sylow1  16081  sylow2blem1  16098  sylow2b  16101  sylow3lem1  16105  sylow3lem2  16106  sylow3lem3  16107  sylow3lem5  16109  sylow3lem6  16110  sylow3  16111  lsmfval  16116  lsmvalx  16117  oppglsm  16120  subglsm  16149  lsmpropd  16153  efgval2  16200  efgi2  16201  efgtlen  16202  efgsdm  16206  efgsdmi  16208  efgsrel  16210  efgs1b  16212  efgsp1  16213  efgsres  16214  efgsfo  16215  efgrelexlemb  16226  frgpnabllem1  16330  iscyg  16335  iscyggen  16336  gsumxp  16441  gsumxpOLD  16443  dprdval  16458  dprdvalOLD  16460  ablfac2  16563  zncyg  17822  cygznlem2a  17841  frlmsplit2  18038  tgrest  18604  ordtval  18634  ordtbas2  18636  ordtcnv  18646  ordtrest  18647  ordtrest2  18649  ispnrm  18784  cmpfi  18852  txval  18978  xkoval  19001  ptval2  19015  ptpjopn  19026  xkoccn  19033  xkoptsub  19068  xkopt  19069  fmval  19357  fmf  19359  txflf  19420  cnextf  19479  subgntr  19518  opnsubg  19519  clsnsg  19521  snclseqg  19527  tsmsval2  19541  tsmsxplem1  19568  ustuqtoplem  19655  utopsnneiplem  19663  utopsnneip  19664  fmucndlem  19707  ressprdsds  19787  mopnval  19854  metuvalOLD  19965  metuval  19966  metdsval  20264  lebnumlem1  20374  lebnumlem3  20376  pi1xfrcnvlem  20469  pi1xfrcnv  20470  minveclem3b  20756  elovolmr  20800  ovolctb  20814  ovoliunlem3  20828  ovolshftlem1  20833  voliunlem3  20874  voliun  20876  volsup  20878  uniioombllem2  20904  uniioombllem3  20906  mbflimsup  20985  itg1climres  21033  itg2monolem1  21069  itg2i1fseq  21074  itg2cnlem1  21080  ellimc2  21193  dvivth  21323  dvne0  21324  lhop2  21328  lhop  21329  evlseu  21367  mdegfval  21415  dchrptlem2  22488  dchrpt  22490  tglnunirn  22862  tgisline  22905  nbgraop  23157  ex-ima  23471  subgornss  23615  efghgrp  23682  isrngo  23687  drngoi  23716  vcoprne  23779  bafval  23804  pj3i  25434  ofrn2  25781  ffsrn  25853  ordtprsval  26201  ordtprsuni  26202  ordtcnvNEW  26203  ordtrestNEW  26204  ordtrest2NEW  26206  qqhval  26256  qqhval2  26264  esumval  26353  esumsn  26368  esumfsupre  26373  sxval  26457  sibf0  26567  sitgfval  26574  cvmlift3lem6  27060  relexprn  27184  trpredeq1  27530  trpredeq2  27531  trpredeq3  27532  mblfinlem2  28270  ovoliunnfl  28274  voliunnfl  28276  filnetlem4  28443  rngohomval  28611  rngoisoval  28624  idlval  28654  pridlval  28674  maxidlval  28680  igenval  28702  mzpmfp  28925  mzpmfpOLD  28926  eldiophb  28937  diophrw  28939  fnrnafv  29911  csbima12gALTOLD  31257  lsatset  32205  docaffvalN  34336  docafvalN  34337