MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rneqd Unicode version

Theorem rneqd 5009
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
StepHypRef Expression
1 rneqd.1 . 2  |-  ( ph  ->  A  =  B )
2 rneq 5007 . 2  |-  ( A  =  B  ->  ran  A  =  ran  B )
31, 2syl 15 1  |-  ( ph  ->  ran  A  =  ran  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1647   ran crn 4793
This theorem is referenced by:  resima2  5091  imaeq1  5110  imaeq2  5111  csbima12gALT  5126  resiima  5132  rnxpid  5212  elxp4  5263  elxp5  5264  funimacnv  5429  fnima  5467  2ndval  6252  fo2nd  6267  f2ndres  6269  curry1  6338  curry2  6341  oarec  6702  en1  7071  xpassen  7099  xpdom2  7100  sbthlem4  7117  fodomr  7155  dffi3  7331  marypha2lem4  7338  ordtypelem9  7388  dfac12lem1  7916  dfac12r  7919  fin23lem32  8117  fin23lem34  8119  fin23lem35  8120  fin23lem36  8121  fin23lem38  8122  fin23lem39  8123  fin23lem41  8125  itunitc  8194  ttukeylem3  8285  fpwwe2lem6  8404  fpwwe2lem9  8407  wunex2  8507  wuncval2  8516  gruima  8571  rpnnen1  10498  hashf1lem1  11591  limsupval  12155  xpnnenOLD  12696  vdwapfval  13226  vdwapval  13228  vdwmc  13233  vdwpc  13235  vdwlem6  13241  vdwlem8  13243  restval  13541  restid2  13545  prdsval  13565  prdsdsval  13587  prdsdsval2  13593  prdsdsval3  13594  imasval  13624  imasdsval  13628  isfull  13994  arwval  14085  gsumvalx  14661  conjsubg  14924  sylow1lem2  15120  sylow1lem4  15122  sylow1  15124  sylow2blem1  15141  sylow2b  15144  sylow3lem1  15148  sylow3lem2  15149  sylow3lem3  15150  sylow3lem5  15152  sylow3lem6  15153  sylow3  15154  lsmfval  15159  lsmvalx  15160  oppglsm  15163  subglsm  15192  lsmpropd  15196  efgval2  15243  efgi2  15244  efgtlen  15245  efgsdm  15249  efgsdmi  15251  efgsrel  15253  efgs1b  15255  efgsp1  15256  efgsres  15257  efgsfo  15258  efgrelexlemb  15269  frgpnabllem1  15371  iscyg  15376  iscyggen  15377  gsumxp  15437  dprdval  15448  ablfac2  15534  zncyg  16719  cygznlem2a  16738  tgrest  17107  ordtval  17136  ordtbas2  17138  ordtcnv  17148  ordtrest  17149  ordtrest2  17151  ispnrm  17284  cmpfi  17352  txval  17476  xkoval  17499  ptval2  17513  ptpjopn  17523  xkoccn  17530  xkoptsub  17565  xkopt  17566  fmval  17851  fmf  17853  txflf  17914  subgntr  18002  opnsubg  18003  clsnsg  18005  snclseqg  18011  tsmsval2  18025  tsmsxplem1  18048  ressprdsds  18148  mopnval  18197  metdsval  18565  lebnumlem1  18674  lebnumlem3  18676  pi1xfrcnvlem  18769  pi1xfrcnv  18770  minveclem3b  19007  elovolmr  19050  ovolctb  19064  ovoliunlem3  19078  ovolshftlem1  19083  voliunlem3  19124  voliun  19126  volsup  19128  uniioombllem2  19153  uniioombllem3  19155  mbflimsup  19236  itg1climres  19284  itg2monolem1  19320  itg2i1fseq  19325  itg2cnlem1  19331  ellimc2  19442  dvivth  19572  dvne0  19573  lhop2  19577  lhop  19578  evlseu  19615  mdegfval  19663  dchrptlem2  20727  dchrpt  20729  ex-ima  21140  subgornss  21284  efghgrp  21351  isrngo  21356  drngoi  21385  vcoprne  21448  bafval  21473  pj3i  23101  xpima  23437  ofrn2  23456  cnextf  23702  ustuqtoplem  23742  utopsnneiplem  23750  fmucndlem  23784  metuval  23792  qqhval  23830  qqhval2  23838  esumval  23906  esumsn  23921  esumfsupre  23926  sxval  24009  cvmlift3lem6  24458  relexprn  24620  trpredeq1  24964  trpredeq2  24965  trpredeq3  24966  ovoliunnfl  25671  voliunnfl  25673  filnetlem4  25837  rngohomval  26101  rngoisoval  26114  idlval  26144  pridlval  26164  maxidlval  26170  igenval  26192  mzpmfp  26331  eldiophb  26342  diophrw  26344  frlmsplit2  26749  pmtrfrn  26906  psgnfval  26929  fnrnafv  27533  nbgraop  27592  nbusgra  27596  lsatset  29251  docaffvalN  31382  docafvalN  31383
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-rab 2637  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-br 4126  df-opab 4180  df-cnv 4800  df-dm 4802  df-rn 4803
  Copyright terms: Public domain W3C validator