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

Theorem rneqd 4906
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 4904 . 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 1623   ran crn 4690
This theorem is referenced by:  resima2  4988  imaeq1  5007  imaeq2  5008  csbima12gALT  5023  resiima  5029  rnxpid  5109  elxp4  5160  elxp5  5161  funimacnv  5324  fnima  5362  2ndval  6125  fo2nd  6140  f2ndres  6142  curry1  6210  curry2  6213  oarec  6560  en1  6928  xpassen  6956  xpdom2  6957  sbthlem4  6974  fodomr  7012  dffi3  7184  marypha2lem4  7191  ordtypelem9  7241  dfac12lem1  7769  dfac12r  7772  fin23lem32  7970  fin23lem34  7972  fin23lem35  7973  fin23lem36  7974  fin23lem38  7975  fin23lem39  7976  fin23lem41  7978  itunitc  8047  ttukeylem3  8138  fpwwe2lem6  8257  fpwwe2lem9  8260  wunex2  8360  wuncval2  8369  gruima  8424  rpnnen1  10347  hashf1lem1  11393  limsupval  11948  xpnnenOLD  12488  vdwapfval  13018  vdwapval  13020  vdwmc  13025  vdwpc  13027  vdwlem6  13033  vdwlem8  13035  restval  13331  restid2  13335  prdsval  13355  prdsdsval  13377  prdsdsval2  13383  prdsdsval3  13384  imasval  13414  imasdsval  13418  isfull  13784  arwval  13875  gsumvalx  14451  conjsubg  14714  sylow1lem2  14910  sylow1lem4  14912  sylow1  14914  sylow2blem1  14931  sylow2b  14934  sylow3lem1  14938  sylow3lem2  14939  sylow3lem3  14940  sylow3lem5  14942  sylow3lem6  14943  sylow3  14944  lsmfval  14949  lsmvalx  14950  oppglsm  14953  subglsm  14982  lsmpropd  14986  efgval2  15033  efgi2  15034  efgtlen  15035  efgsdm  15039  efgsdmi  15041  efgsrel  15043  efgs1b  15045  efgsp1  15046  efgsres  15047  efgsfo  15048  efgrelexlemb  15059  frgpnabllem1  15161  iscyg  15166  iscyggen  15167  gsumxp  15227  dprdval  15238  ablfac2  15324  zncyg  16502  cygznlem2a  16521  tgrest  16890  ordtval  16919  ordtbas2  16921  ordtcnv  16931  ordtrest  16932  ordtrest2  16934  ispnrm  17067  cmpfi  17135  txval  17259  xkoval  17282  ptval2  17296  ptpjopn  17306  xkoccn  17313  xkoptsub  17348  xkopt  17349  fmval  17638  fmf  17640  txflf  17701  subgntr  17789  opnsubg  17790  clsnsg  17792  snclseqg  17798  tsmsval2  17812  tsmsxplem1  17835  ressprdsds  17935  mopnval  17984  metdsval  18351  lebnumlem1  18459  lebnumlem3  18461  pi1xfrcnvlem  18554  pi1xfrcnv  18555  minveclem3b  18792  elovolmr  18835  ovolctb  18849  ovoliunlem3  18863  ovolshftlem1  18868  voliunlem3  18909  voliun  18911  volsup  18913  uniioombllem2  18938  uniioombllem3  18940  mbflimsup  19021  itg1climres  19069  itg2monolem1  19105  itg2i1fseq  19110  itg2cnlem1  19116  ellimc2  19227  dvivth  19357  dvne0  19358  lhop2  19362  lhop  19363  evlseu  19400  mdegfval  19448  dchrptlem2  20504  dchrpt  20506  ex-ima  20829  subgornss  20973  efghgrp  21040  isrngo  21045  drngoi  21074  vcoprne  21135  bafval  21160  pj3i  22788  xpima  23202  ofrn2  23207  esumval  23425  esumsn  23437  sxval  23521  dya2iocrrnval  23582  isibfm  23593  cvmlift3lem6  23855  relexprn  24033  trpredeq1  24223  trpredeq2  24224  trpredeq3  24225  iscst1  25174  iscst2  25175  domrancur1b  25200  domrancur1c  25202  prsubrtr  25399  svs3  25488  aidm2  25750  prismorcsetlem  25912  prismorcset  25914  filnetlem4  26330  rngohomval  26595  rngoisoval  26608  idlval  26638  pridlval  26658  maxidlval  26664  igenval  26686  mzpmfp  26825  eldiophb  26836  diophrw  26838  frlmsplit2  27243  pmtrfrn  27400  psgnfval  27423  fnrnafv  28024  nbgraop  28140  nbusgra  28143  lsatset  29180  docaffvalN  31311  docafvalN  31312
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-cnv 4697  df-dm 4699  df-rn 4700
  Copyright terms: Public domain W3C validator