Theorem rneqd 5216

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

Syntax hints:   -> wi 4   = wceq 1381   ran crn 4986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-br 4434  df-opab 4492  df-cnv 4993  df-dm 4995  df-rn 4996

This theorem is referenced by:  resima2  5293  imaeq1  5318  imaeq2  5319  resiima  5337  rnxpid  5426  xpima  5435  funimacnv  5646  fnima  5685  elxp4  6725  elxp5  6726  2ndval  6784  fo2nd  6802  f2ndres  6804  curry1  6873  curry2  6876  oarec  7209  en1  7580  xpassen  7609  xpdom2  7610  sbthlem4  7628  fodomr  7666  dffi3  7889  marypha2lem4  7896  ordtypelem9  7949  dfac12lem1  8521  dfac12r  8524  fin23lem32  8722  fin23lem34  8724  fin23lem35  8725  fin23lem36  8726  fin23lem38  8727  fin23lem39  8728  fin23lem41  8730  itunitc  8799  ttukeylem3  8889  fpwwe2lem6  9011  fpwwe2lem9  9014  wunex2  9114  wuncval2  9123  gruima  9178  rpnnen1  11217  hashf1lem1  12478  s1rn  12585  limsupval  13271  xpnnenOLD  13815  vdwapfval  14361  vdwapval  14363  vdwmc  14368  vdwpc  14370  vdwlem6  14376  vdwlem8  14378  restval  14696  restid2  14700  prdsval  14724  prdsdsval  14747  prdsdsval2  14753  prdsdsval3  14754  imasval  14780  imasdsval  14784  isfull  15148  arwval  15239  gsumvalx  15766  conjsubg  16167  pmtrfrn  16352  psgnfval  16394  sylow1lem2  16488  sylow1lem4  16490  sylow1  16492  sylow2blem1  16509  sylow2b  16512  sylow3lem1  16516  sylow3lem2  16517  sylow3lem3  16518  sylow3lem5  16520  sylow3lem6  16521  sylow3  16522  lsmfval  16527  lsmvalx  16528  oppglsm  16531  subglsm  16560  lsmpropd  16564  efgval2  16611  efgi2  16612  efgtlen  16613  efgsdm  16617  efgsdmi  16619  efgsrel  16621  efgs1b  16623  efgsp1  16624  efgsres  16625  efgsfo  16626  efgrelexlemb  16637  frgpnabllem1  16746  iscyg  16751  iscyggen  16752  gsumxp  16873  gsumxpOLD  16875  dprdval  16903  dprdvalOLD  16905  ablfac2  17008  evlseu  18053  zncyg  18454  cygznlem2a  18473  frlmsplit2  18670  tgrest  19526  ordtval  19556  ordtbas2  19558  ordtcnv  19568  ordtrest  19569  ordtrest2  19571  ispnrm  19706  cmpfi  19774  txval  19931  xkoval  19954  ptval2  19968  ptpjopn  19979  xkoccn  19986  xkoptsub  20021  xkopt  20022  fmval  20310  fmf  20312  txflf  20373  cnextf  20432  subgntr  20471  opnsubg  20472  clsnsg  20474  snclseqg  20480  tsmsval2  20494  tsmsxplem1  20521  ustuqtoplem  20608  utopsnneiplem  20616  utopsnneip  20617  fmucndlem  20660  ressprdsds  20740  mopnval  20807  metuvalOLD  20918  metuval  20919  metdsval  21217  lebnumlem1  21327  lebnumlem3  21329  pi1xfrcnvlem  21422  pi1xfrcnv  21423  minveclem3b  21709  elovolmr  21753  ovolctb  21767  ovoliunlem3  21781  ovolshftlem1  21786  voliunlem3  21828  voliun  21830  volsup  21832  uniioombllem2  21858  uniioombllem3  21860  mbflimsup  21939  itg1climres  21987  itg2monolem1  22023  itg2i1fseq  22028  itg2cnlem1  22034  ellimc2  22147  dvivth  22277  dvne0  22278  lhop2  22282  lhop  22283  mdegfval  22326  dchrptlem2  23405  dchrpt  23407  tglnunirn  23800  tgisline  23872  perpln1  23952  perpln2  23953  isperp  23954  ishpg  23993  lmif  24016  islmib  24018  edgval  24204  edgopval  24205  edgss  24217  nbgraop  24288  nbgraopALT  24289  ex-ima  25028  subgornss  25173  efghgrpOLD  25240  isrngo  25245  drngoi  25274  vcoprne  25337  bafval  25362  pj3i  26992  ofrn2  27345  ffsrn  27417  ordtprsval  27766  ordtprsuni  27767  ordtcnvNEW  27768  ordtrestNEW  27769  ordtrest2NEW  27771  qqhval  27821  qqhval2  27829  esumval  27923  esumsn  27938  esumfsupre  27943  sxval  28027  omsval  28130  omsfval  28131  sibf0  28142  sitgfval  28149  cvmlift3lem6  28635  mvtval  28726  mvrsval  28731  mrsubrn  28739  mrsub0  28742  mrsubf  28743  mrsubccat  28744  mrsubcn  28745  mrsubco  28747  mrsubvrs  28748  elmsubrn  28754  msubrn  28755  msubf  28758  mstaval  28770  msubvrs  28786  mclsval  28789  relexprn  28925  trpredeq1  29271  trpredeq2  29272  trpredeq3  29273  mblfinlem2  30020  ovoliunnfl  30024  voliunnfl  30026  filnetlem4  30167  rngohomval  30335  rngoisoval  30348  idlval  30378  pridlval  30398  maxidlval  30404  igenval  30426  mzpmfp  30647  mzpmfpOLD  30648  eldiophb  30658  diophrw  30660  fourierdlem60  31834  fourierdlem61  31835  fnrnafv  32081  csbima12gALTOLD  33330  lsatset  34417  docaffvalN  36550  docafvalN  36551  conrel1d  37426