Theorem rneqd 5061

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

Syntax hints:   -> wi 4   = wceq 1443   ran crn 4834

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-br 4402  df-opab 4461  df-cnv 4841  df-dm 4843  df-rn 4844

This theorem is referenced by:  resima2  5137  imaeq1  5162  imaeq2  5163  resiima  5181  rnxpid  5269  xpima  5278  funimacnv  5653  fnima  5692  elxp4  6734  elxp5  6735  2ndval  6793  fo2nd  6811  f2ndres  6813  curry1  6885  curry2  6888  oarec  7260  en1  7633  xpassen  7663  xpdom2  7664  sbthlem4  7682  fodomr  7720  dffi3  7942  marypha2lem4  7949  ordtypelem9  8038  dfac12lem1  8570  dfac12r  8573  fin23lem32  8771  fin23lem34  8773  fin23lem35  8774  fin23lem36  8775  fin23lem38  8776  fin23lem39  8777  fin23lem41  8779  itunitc  8848  ttukeylem3  8938  fpwwe2lem6  9057  fpwwe2lem9  9060  wunex2  9160  wuncval2  9169  gruima  9224  rpnnen1  11292  hashf1lem1  12615  s1rn  12735  relexprng  13102  relexpfld  13105  limsupval  13524  limsupvalOLD  13525  vdwapfval  14914  vdwapval  14916  vdwmc  14921  vdwpc  14923  vdwlem6  14929  vdwlem8  14931  restval  15318  restid2  15322  prdsval  15346  prdsdsval  15369  prdsdsval2  15375  prdsdsval3  15376  imasval  15404  imasvalOLD  15405  imasdsval  15409  imasdsvalOLD  15421  isfull  15808  arwval  15931  gsumvalx  16506  conjsubg  16907  pmtrfrn  17092  psgnfval  17134  sylow1lem2  17244  sylow1lem4  17246  sylow1  17248  sylow2blem1  17265  sylow2b  17268  sylow3lem1  17272  sylow3lem2  17273  sylow3lem3  17274  sylow3lem5  17276  sylow3lem6  17277  sylow3  17278  lsmfval  17283  lsmvalx  17284  oppglsm  17287  subglsm  17316  lsmpropd  17320  efgval2  17367  efgi2  17368  efgtlen  17369  efgsdm  17373  efgsdmi  17375  efgsrel  17377  efgs1b  17379  efgsp1  17380  efgsres  17381  efgsfo  17382  efgrelexlemb  17393  frgpnabllem1  17502  iscyg  17507  iscyggen  17508  gsumxp  17601  dprdval  17628  ablfac2  17715  evlseu  18732  zncyg  19112  cygznlem2a  19131  frlmsplit2  19324  tgrest  20168  ordtval  20198  ordtbas2  20200  ordtcnv  20210  ordtrest  20211  ordtrest2  20213  ispnrm  20348  cmpfi  20416  txval  20572  xkoval  20595  ptval2  20609  ptpjopn  20620  xkoccn  20627  xkoptsub  20662  xkopt  20663  fmval  20951  fmf  20953  txflf  21014  cnextf  21074  subgntr  21114  opnsubg  21115  clsnsg  21117  snclseqg  21123  tsmsval2  21137  tsmsxplem1  21160  ustuqtoplem  21247  utopsnneiplem  21255  utopsnneip  21256  fmucndlem  21299  ressprdsds  21379  mopnval  21446  metuval  21557  metdsval  21857  metdsvalOLD  21872  lebnumlem1  21982  lebnumlem3  21984  lebnumlem1OLD  21985  lebnumlem3OLD  21987  pi1xfrcnvlem  22080  pi1xfrcnv  22081  minveclem3b  22363  minveclem3bOLD  22375  elovolmr  22422  ovolctb  22436  ovoliunlem3  22450  ovolshftlem1  22455  voliunlem3  22498  voliun  22500  volsup  22502  uniioombllem2  22533  uniioombllem2OLD  22534  uniioombllem3  22536  mbflimsup  22616  mbflimsupOLD  22617  itg1climres  22665  itg2monolem1  22701  itg2i1fseq  22706  itg2cnlem1  22712  ellimc2  22825  dvivth  22955  dvne0  22956  lhop2  22960  lhop  22961  mdegfval  23004  dchrptlem2  24186  dchrpt  24188  tglnunirn  24586  tgisline  24665  perpln1  24748  perpln2  24749  isperp  24750  ishpg  24794  lmif  24820  islmib  24822  edgval  25059  edgopval  25060  edgss  25072  nbgraop  25144  nbgraopALT  25145  ex-ima  25885  subgornss  26027  efghgrpOLD  26094  isrngo  26099  drngoi  26128  vcoprne  26191  bafval  26216  pj3i  27854  ofrn2  28234  ffsrn  28307  smatrcl  28615  ordtprsval  28717  ordtprsuni  28718  ordtcnvNEW  28719  ordtrestNEW  28720  ordtrest2NEW  28722  qqhval  28771  qqhval2  28779  esumval  28860  esumsnf  28878  esumrnmpt2  28882  esumfsupre  28885  esumsup  28903  sxval  29005  omsval  29110  omsfval  29111  omsvalOLD  29114  omsfvalOLD  29115  carsggect  29143  sibf0  29160  sitgfval  29167  cvmlift3lem6  30040  mvtval  30131  mvrsval  30136  mrsubrn  30144  mrsub0  30147  mrsubf  30148  mrsubccat  30149  mrsubcn  30150  mrsubco  30152  mrsubvrs  30153  elmsubrn  30159  msubrn  30160  msubf  30163  mstaval  30175  msubvrs  30191  mclsval  30194  trpredeq1  30454  trpredeq2  30455  trpredeq3  30456  filnetlem4  31030  mptsnunlem  31733  dissneqlem  31735  poimirlem3  31936  poimirlem9  31942  poimirlem16  31949  poimirlem17  31950  poimirlem19  31952  poimirlem20  31953  poimirlem24  31957  poimirlem30  31963  poimirlem32  31965  mblfinlem2  31971  ovoliunnfl  31975  voliunnfl  31977  rngohomval  32196  rngoisoval  32209  idlval  32239  pridlval  32259  maxidlval  32265  igenval  32287  lsatset  32550  docaffvalN  34683  docafvalN  34684  mzpmfp  35583  eldiophb  35593  diophrw  35595  conrel1d  36249  iunrelexp0  36288  rntrclfv  36318  csbima12gALTOLD  37212  rnsnf  37452  fourierdlem60  38024  fourierdlem61  38025  sge0val  38202  sge0z  38211  sge0revalmpt  38214  sge0tsms  38216  sge0sup  38227  sge0split  38245  sge0fodjrnlem  38252  meadjiunlem  38297  omeiunle  38332  fnrnafv  38658  edgaval  39198  edgaopval  39199  edgastruct  39201  edgiedgb  39202  edg0iedg0  39204  usgr2edg  39277  usgr1e  39306  cplgrop  39487  cusgrexi  39490  umgr2v2eedg  39544