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

Theorem rneqd 5100
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 5098 . 2  |-  ( A  =  B  ->  ran  A  =  ran  B )
31, 2syl 16 1  |-  ( ph  ->  ran  A  =  ran  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   ran crn 4882
This theorem is referenced by:  resima2  5182  imaeq1  5201  imaeq2  5202  csbima12gALT  5217  resiima  5223  rnxpid  5305  xpima  5316  elxp4  5360  elxp5  5361  funimacnv  5528  fnima  5566  2ndval  6355  fo2nd  6370  f2ndres  6372  curry1  6441  curry2  6444  oarec  6808  en1  7177  xpassen  7205  xpdom2  7206  sbthlem4  7223  fodomr  7261  dffi3  7439  marypha2lem4  7446  ordtypelem9  7498  dfac12lem1  8028  dfac12r  8031  fin23lem32  8229  fin23lem34  8231  fin23lem35  8232  fin23lem36  8233  fin23lem38  8234  fin23lem39  8235  fin23lem41  8237  itunitc  8306  ttukeylem3  8396  fpwwe2lem6  8515  fpwwe2lem9  8518  wunex2  8618  wuncval2  8627  gruima  8682  rpnnen1  10610  hashf1lem1  11709  limsupval  12273  xpnnenOLD  12814  vdwapfval  13344  vdwapval  13346  vdwmc  13351  vdwpc  13353  vdwlem6  13359  vdwlem8  13361  restval  13659  restid2  13663  prdsval  13683  prdsdsval  13705  prdsdsval2  13711  prdsdsval3  13712  imasval  13742  imasdsval  13746  isfull  14112  arwval  14203  gsumvalx  14779  conjsubg  15042  sylow1lem2  15238  sylow1lem4  15240  sylow1  15242  sylow2blem1  15259  sylow2b  15262  sylow3lem1  15266  sylow3lem2  15267  sylow3lem3  15268  sylow3lem5  15270  sylow3lem6  15271  sylow3  15272  lsmfval  15277  lsmvalx  15278  oppglsm  15281  subglsm  15310  lsmpropd  15314  efgval2  15361  efgi2  15362  efgtlen  15363  efgsdm  15367  efgsdmi  15369  efgsrel  15371  efgs1b  15373  efgsp1  15374  efgsres  15375  efgsfo  15376  efgrelexlemb  15387  frgpnabllem1  15489  iscyg  15494  iscyggen  15495  gsumxp  15555  dprdval  15566  ablfac2  15652  zncyg  16834  cygznlem2a  16853  tgrest  17228  ordtval  17258  ordtbas2  17260  ordtcnv  17270  ordtrest  17271  ordtrest2  17273  ispnrm  17408  cmpfi  17476  txval  17601  xkoval  17624  ptval2  17638  ptpjopn  17649  xkoccn  17656  xkoptsub  17691  xkopt  17692  fmval  17980  fmf  17982  txflf  18043  cnextf  18102  subgntr  18141  opnsubg  18142  clsnsg  18144  snclseqg  18150  tsmsval2  18164  tsmsxplem1  18187  ustuqtoplem  18274  utopsnneiplem  18282  utopsnneip  18283  fmucndlem  18326  ressprdsds  18406  mopnval  18473  metuvalOLD  18584  metuval  18585  metdsval  18882  lebnumlem1  18991  lebnumlem3  18993  pi1xfrcnvlem  19086  pi1xfrcnv  19087  minveclem3b  19334  elovolmr  19377  ovolctb  19391  ovoliunlem3  19405  ovolshftlem1  19410  voliunlem3  19451  voliun  19453  volsup  19455  uniioombllem2  19480  uniioombllem3  19482  mbflimsup  19561  itg1climres  19609  itg2monolem1  19645  itg2i1fseq  19650  itg2cnlem1  19656  ellimc2  19769  dvivth  19899  dvne0  19900  lhop2  19904  lhop  19905  evlseu  19942  mdegfval  19990  dchrptlem2  21054  dchrpt  21056  nbgraop  21441  ex-ima  21755  subgornss  21899  efghgrp  21966  isrngo  21971  drngoi  22000  vcoprne  22063  bafval  22088  pj3i  23716  ofrn2  24058  qqhval  24363  qqhval2  24371  esumval  24446  esumsn  24461  esumfsupre  24466  sxval  24549  sibf0  24654  sitgfval  24660  cvmlift3lem6  25016  relexprn  25141  trpredeq1  25503  trpredeq2  25504  trpredeq3  25505  mblfinlem2  26256  ovoliunnfl  26260  voliunnfl  26262  filnetlem4  26424  rngohomval  26594  rngoisoval  26607  idlval  26637  pridlval  26657  maxidlval  26663  igenval  26685  mzpmfp  26818  eldiophb  26829  diophrw  26831  frlmsplit2  27234  pmtrfrn  27391  psgnfval  27414  fnrnafv  28016  lsatset  29862  docaffvalN  31993  docafvalN  31994
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4216  df-opab 4270  df-cnv 4889  df-dm 4891  df-rn 4892
  Copyright terms: Public domain W3C validator