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

Theorem rneq 5233
Description: Equality theorem for range. (Contributed by NM, 29-Dec-1996.)
Assertion
Ref Expression
rneq

Proof of Theorem rneq
StepHypRef Expression
1 cnveq 5181 . . 3
21dmeqd 5210 . 2
3 df-rn 5015 . 2
4 df-rn 5015 . 2
52, 3, 43eqtr4g 2523 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  `'ccnv 5003  domcdm 5004  rancrn 5005
This theorem is referenced by:  rneqi  5234  rneqd  5235  feq1  5718  foeq1  5796  fnrnfv  5919  fconst5  6128  frxp  6910  tz7.44-2  7092  tz7.44-3  7093  ixpsnf1o  7529  ordtypecbv  7963  ordtypelem3  7966  dfac8alem  8431  dfac8a  8432  dfac5lem3  8527  dfac9  8537  dfac12lem1  8544  dfac12r  8547  ackbij2  8644  isfin3ds  8730  fin23lem17  8739  fin23lem29  8742  fin23lem30  8743  fin23lem32  8745  fin23lem34  8747  fin23lem35  8748  fin23lem39  8751  fin23lem41  8753  isf33lem  8767  isf34lem6  8781  dcomex  8848  axdc2lem  8849  zorn2lem1  8897  zorn2g  8904  ttukey2g  8917  gruurn  9197  rpnnen1  11242  mpfrcl  18187  ply1frcl  18355  pnrmopn  19844  isi1f  22081  itg1val  22090  axlowdimlem13  24257  axlowdim1  24262  iscusgra  24456  isuvtx  24488  wwlk  24681  clwwlk  24766  rusgra0edg  24955  isfrgra  24990  ex-rn  25161  gidval  25215  grpoinvfval  25226  grpodivfval  25244  gxfval  25259  isablo  25285  elghomlem1OLD  25363  iscom2  25414  isdivrngo  25433  vci  25441  isvclem  25470  isnvlem  25503  isphg  25732  pj11i  26629  hmopidmch  27072  hmopidmpj  27073  pjss1coi  27082  locfinreflem  27843  locfinref  27844  issibf  28275  sitgfval  28283  mrsubvrs  28882  ghomgrplem  29029  elgiso  29036  relexprn  29059  dfrtrcl2  29071  rdgprc0  29226  rdgprc  29227  dfrdg2  29228  brrangeg  29586  volsupnfl  30059  dnnumch1  30990  aomclem3  31002  aomclem8  31007  csbima12gALTVD  33697
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-cnv 5012  df-dm 5014  df-rn 5015
  Copyright terms: Public domain W3C validator