Theorem rneqd 5082

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

Syntax hints:   -> wi 4   = wceq 1437   ran crn 4855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-br 4427  df-opab 4485  df-cnv 4862  df-dm 4864  df-rn 4865

This theorem is referenced by:  resima2  5158  imaeq1  5183  imaeq2  5184  resiima  5202  rnxpid  5290  xpima  5299  funimacnv  5673  fnima  5712  elxp4  6751  elxp5  6752  2ndval  6810  fo2nd  6828  f2ndres  6830  curry1  6899  curry2  6902  oarec  7271  en1  7643  xpassen  7672  xpdom2  7673  sbthlem4  7691  fodomr  7729  dffi3  7951  marypha2lem4  7958  ordtypelem9  8041  dfac12lem1  8571  dfac12r  8574  fin23lem32  8772  fin23lem34  8774  fin23lem35  8775  fin23lem36  8776  fin23lem38  8777  fin23lem39  8778  fin23lem41  8780  itunitc  8849  ttukeylem3  8939  fpwwe2lem6  9059  fpwwe2lem9  9062  wunex2  9162  wuncval2  9171  gruima  9226  rpnnen1  11295  hashf1lem1  12613  s1rn  12725  relexprng  13088  relexpfld  13091  limsupval  13509  limsupvalOLD  13510  vdwapfval  14884  vdwapval  14886  vdwmc  14891  vdwpc  14893  vdwlem6  14899  vdwlem8  14901  restval  15284  restid2  15288  prdsval  15312  prdsdsval  15335  prdsdsval2  15341  prdsdsval3  15342  imasval  15368  imasdsval  15372  isfull  15766  arwval  15889  gsumvalx  16464  conjsubg  16865  pmtrfrn  17050  psgnfval  17092  sylow1lem2  17186  sylow1lem4  17188  sylow1  17190  sylow2blem1  17207  sylow2b  17210  sylow3lem1  17214  sylow3lem2  17215  sylow3lem3  17216  sylow3lem5  17218  sylow3lem6  17219  sylow3  17220  lsmfval  17225  lsmvalx  17226  oppglsm  17229  subglsm  17258  lsmpropd  17262  efgval2  17309  efgi2  17310  efgtlen  17311  efgsdm  17315  efgsdmi  17317  efgsrel  17319  efgs1b  17321  efgsp1  17322  efgsres  17323  efgsfo  17324  efgrelexlemb  17335  frgpnabllem1  17444  iscyg  17449  iscyggen  17450  gsumxp  17543  dprdval  17570  ablfac2  17657  evlseu  18674  zncyg  19050  cygznlem2a  19069  frlmsplit2  19262  tgrest  20106  ordtval  20136  ordtbas2  20138  ordtcnv  20148  ordtrest  20149  ordtrest2  20151  ispnrm  20286  cmpfi  20354  txval  20510  xkoval  20533  ptval2  20547  ptpjopn  20558  xkoccn  20565  xkoptsub  20600  xkopt  20601  fmval  20889  fmf  20891  txflf  20952  cnextf  21012  subgntr  21052  opnsubg  21053  clsnsg  21055  snclseqg  21061  tsmsval2  21075  tsmsxplem1  21098  ustuqtoplem  21185  utopsnneiplem  21193  utopsnneip  21194  fmucndlem  21237  ressprdsds  21317  mopnval  21384  metuval  21495  metdsval  21775  lebnumlem1  21885  lebnumlem3  21887  pi1xfrcnvlem  21980  pi1xfrcnv  21981  minveclem3b  22263  elovolmr  22307  ovolctb  22321  ovoliunlem3  22335  ovolshftlem1  22340  voliunlem3  22382  voliun  22384  volsup  22386  uniioombllem2  22417  uniioombllem2OLD  22418  uniioombllem3  22420  mbflimsup  22500  mbflimsupOLD  22501  itg1climres  22549  itg2monolem1  22585  itg2i1fseq  22590  itg2cnlem1  22596  ellimc2  22709  dvivth  22839  dvne0  22840  lhop2  22844  lhop  22845  mdegfval  22888  dchrptlem2  24056  dchrpt  24058  tglnunirn  24453  tgisline  24531  perpln1  24612  perpln2  24613  isperp  24614  ishpg  24657  lmif  24683  islmib  24685  edgval  24912  edgopval  24913  edgss  24925  nbgraop  24996  nbgraopALT  24997  ex-ima  25737  subgornss  25879  efghgrpOLD  25946  isrngo  25951  drngoi  25980  vcoprne  26043  bafval  26068  pj3i  27696  ofrn2  28081  ffsrn  28157  smatrcl  28461  ordtprsval  28563  ordtprsuni  28564  ordtcnvNEW  28565  ordtrestNEW  28566  ordtrest2NEW  28568  qqhval  28617  qqhval2  28625  esumval  28706  esumsnf  28724  esumrnmpt2  28728  esumfsupre  28731  esumsup  28749  sxval  28851  omsval  28954  omsfval  28955  carsggect  28979  sibf0  28995  sitgfval  29002  cvmlift3lem6  29835  mvtval  29926  mvrsval  29931  mrsubrn  29939  mrsub0  29942  mrsubf  29943  mrsubccat  29944  mrsubcn  29945  mrsubco  29947  mrsubvrs  29948  elmsubrn  29954  msubrn  29955  msubf  29958  mstaval  29970  msubvrs  29986  mclsval  29989  trpredeq1  30248  trpredeq2  30249  trpredeq3  30250  filnetlem4  30822  mptsnunlem  31474  dissneqlem  31476  poimirlem3  31647  poimirlem9  31653  poimirlem16  31660  poimirlem17  31661  poimirlem19  31663  poimirlem20  31664  poimirlem24  31668  poimirlem30  31674  poimirlem32  31676  mblfinlem2  31682  ovoliunnfl  31686  voliunnfl  31688  rngohomval  31907  rngoisoval  31920  idlval  31950  pridlval  31970  maxidlval  31976  igenval  31998  lsatset  32265  docaffvalN  34398  docafvalN  34399  mzpmfp  35298  eldiophb  35308  diophrw  35310  conrel1d  35894  iunrelexp0  35933  rntrclfv  35963  csbima12gALTOLD  36858  rnsnf  37081  fourierdlem60  37598  fourierdlem61  37599  sge0val  37742  sge0z  37751  sge0revalmpt  37754  sge0tsms  37756  sge0sup  37767  sge0split  37785  sge0fodjrnlem  37792  meadjiunlem  37812  omeiunle  37847  fnrnafv  38054