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

Theorem resdm 5232
Description: A relation restricted to its domain equals itself. (Contributed by NM, 12-Dec-2006.)
Assertion
Ref Expression
resdm  |-  ( Rel 
A  ->  ( A  |` 
dom  A )  =  A )

Proof of Theorem resdm
StepHypRef Expression
1 ssid 3459 . 2  |-  dom  A  C_ 
dom  A
2 relssres 5231 . 2  |-  ( ( Rel  A  /\  dom  A 
C_  dom  A )  ->  ( A  |`  dom  A
)  =  A )
31, 2mpan2 671 1  |-  ( Rel 
A  ->  ( A  |` 
dom  A )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    C_ wss 3412   dom cdm 4924    |` cres 4926   Rel wrel 4929
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-sep 4497  ax-nul 4505  ax-pr 4615
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-rab 2801  df-v 3056  df-dif 3415  df-un 3417  df-in 3419  df-ss 3426  df-nul 3722  df-if 3876  df-sn 3962  df-pr 3964  df-op 3968  df-br 4377  df-opab 4435  df-xp 4930  df-rel 4931  df-dm 4934  df-res 4936
This theorem is referenced by:  resindm  5235  resdm2  5412  relresfld  5448  relcoi1  5450  fnex  6029  dftpos2  6848  tfrlem11  6933  tfrlem15  6937  tfrlem16  6938  pmresg  7326  domss2  7556  axdc3lem4  8709  gruima  9056  funsseq  27700  seff  29719  sblpnf  29720  resisresindm  30263  bnj1321  32300
  Copyright terms: Public domain W3C validator