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

Theorem rneq 4983
Description: Equality theorem for range. (Contributed by NM, 29-Dec-1996.)
Assertion
Ref Expression
rneq  |-  ( A  =  B  ->  ran  A  =  ran  B )

Proof of Theorem rneq
StepHypRef Expression
1 cnveq 4934 . . 3  |-  ( A  =  B  ->  `' A  =  `' B
)
21dmeqd 4960 . 2  |-  ( A  =  B  ->  dom  `' A  =  dom  `' B )
3 df-rn 4779 . 2  |-  ran  A  =  dom  `' A
4 df-rn 4779 . 2  |-  ran  B  =  dom  `' B
52, 3, 43eqtr4g 2415 1  |-  ( A  =  B  ->  ran  A  =  ran  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642   `'ccnv 4767   dom cdm 4768   ran crn 4769
This theorem is referenced by:  rneqi  4984  rneqd  4985  feq1  5454  foeq1  5527  fnrnfv  5649  fconst5  5812  frxp  6309  tz7.44-2  6504  tz7.44-3  6505  map0e  6890  ixpsnf1o  6941  ordtypecbv  7319  ordtypelem3  7322  dfac8alem  7743  dfac8a  7744  dfac5lem3  7839  dfac9  7849  dfac12lem1  7856  dfac12r  7859  ackbij2  7956  isfin3ds  8042  fin23lem17  8051  fin23lem29  8054  fin23lem30  8055  fin23lem32  8057  fin23lem34  8059  fin23lem35  8060  fin23lem39  8063  fin23lem41  8065  isf33lem  8079  isf34lem6  8093  dcomex  8160  axdc2lem  8161  zorn2lem1  8210  zorn2g  8217  ttukey2g  8230  gruurn  8507  rpnnen1  10436  pnrmopn  17171  isi1f  19127  itg1val  19136  mpfrcl  19500  ex-rn  20933  gidval  20986  grpoinvfval  20997  grpodivfval  21015  gxfval  21030  isablo  21056  elghomlem1  21134  iscom2  21185  isdivrngo  21204  vci  21212  isvclem  21241  isnvlem  21274  isphg  21503  pj11i  22398  hmopidmch  22841  hmopidmpj  22842  pjss1coi  22851  ghomgrplem  24400  elgiso  24407  relexprn  24437  dfrtrcl2  24449  rdgprc0  24708  rdgprc  24709  dfrdg2  24710  brrangeg  25033  axlowdimlem13  25141  axlowdim1  25146  volsupnfl  25491  dnnumch1  26464  aomclem3  26476  aomclem8  26482  iscusgra  27611  isuvtx  27634  isfrgra  27806  csbima12gALTVD  28418
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-br 4103  df-opab 4157  df-cnv 4776  df-dm 4778  df-rn 4779
  Copyright terms: Public domain W3C validator