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

Theorem rneq 5804
 Description: Equality theorem for range. (Contributed by NM, 29-Dec-1996.)
Assertion
Ref Expression
rneq (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Proof of Theorem rneq
StepHypRef Expression
1 cnveq 5742 . . 3 (𝐴 = 𝐵𝐴 = 𝐵)
21dmeqd 5772 . 2 (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
3 df-rn 5564 . 2 ran 𝐴 = dom 𝐴
4 df-rn 5564 . 2 ran 𝐵 = dom 𝐵
52, 3, 43eqtr4g 2885 1 (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1530  ◡ccnv 5552  dom cdm 5553  ran crn 5554 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-br 5063  df-opab 5125  df-cnv 5561  df-dm 5563  df-rn 5564 This theorem is referenced by:  rneqi  5805  rneqd  5806  feq1  6491  foeq1  6582  fnrnfv  6721  fconst5  6967  frxp  7814  tz7.44-2  8037  tz7.44-3  8038  ixpsnf1o  8494  ordtypecbv  8973  ordtypelem3  8976  dfac8alem  9447  dfac8a  9448  dfac5lem3  9543  dfac9  9554  dfac12lem1  9561  dfac12r  9564  ackbij2  9657  isfin3ds  9743  fin23lem17  9752  fin23lem29  9755  fin23lem30  9756  fin23lem32  9758  fin23lem34  9760  fin23lem35  9761  fin23lem39  9764  fin23lem41  9766  isf33lem  9780  isf34lem6  9794  dcomex  9861  axdc2lem  9862  zorn2lem1  9910  zorn2g  9917  ttukey2g  9930  gruurn  10212  rpnnen1lem6  12374  relexp0g  14374  relexpsucnnr  14377  dfrtrcl2  14414  mpfrcl  20219  selvval  20251  ply1frcl  20401  pnrmopn  21870  isi1f  24193  itg1val  24202  axlowdimlem13  26657  axlowdim1  26662  ausgrusgri  26870  0uhgrsubgr  26978  cusgrsize  27153  ex-rn  28136  gidval  28206  grpoinvfval  28216  grpodivfval  28228  isablo  28240  vciOLD  28255  isvclem  28271  isnvlem  28304  isphg  28511  pj11i  29405  hmopidmch  29847  hmopidmpj  29848  pjss1coi  29857  padct  30371  tocyc01  30677  tocyccntz  30703  locfinreflem  30993  locfinref  30994  issibf  31480  sitgfval  31488  mrsubvrs  32656  rdgprc0  32925  rdgprc  32926  dfrdg2  32927  madeval  33176  brrangeg  33284  poimirlem24  34786  volsupnfl  34807  elghomlem1OLD  35034  isdivrngo  35099  iscom2  35144  elrefrels2  35627  elrefrels3  35628  refreleq  35630  elcnvrefrels2  35640  elcnvrefrels3  35641  dnnumch1  39512  aomclem3  39524  aomclem8  39529  rclexi  39843  rtrclex  39845  rtrclexi  39849  cnvrcl0  39853  dfrtrcl5  39857  dfrcl2  39887  csbima12gALTVD  41099  unirnmap  41339  ssmapsn  41347  sge0val  42517  vonvolmbl  42812
 Copyright terms: Public domain W3C validator