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

Theorem ssdmres 5132
Description: A domain restricted to a subclass equals the subclass. (Contributed by NM, 2-Mar-1997.)
Assertion
Ref Expression
ssdmres  |-  ( A 
C_  dom  B  <->  dom  ( B  |`  A )  =  A )

Proof of Theorem ssdmres
StepHypRef Expression
1 df-ss 3404 . 2  |-  ( A 
C_  dom  B  <->  ( A  i^i  dom  B )  =  A )
2 dmres 5131 . . 3  |-  dom  ( B  |`  A )  =  ( A  i^i  dom  B )
32eqeq1i 2476 . 2  |-  ( dom  ( B  |`  A )  =  A  <->  ( A  i^i  dom  B )  =  A )
41, 3bitr4i 260 1  |-  ( A 
C_  dom  B  <->  dom  ( B  |`  A )  =  A )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    = wceq 1452    i^i cin 3389    C_ wss 3390   dom cdm 4839    |` cres 4841
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396  df-opab 4455  df-xp 4845  df-dm 4849  df-res 4851
This theorem is referenced by:  dmresi  5166  fnssresb  5698  fores  5815  foimacnv  5845  dffv2  5953  sbthlem4  7703  hashimarn  12651  dvres3  22947  c1liplem1  23027  lhop1lem  23044  lhop  23047  usgrares1  25217  usgrafilem1  25218  resgrprn  26089  hhssabloi  26994  hhssnv  26996  hhshsslem1  26999  fresf1o  28307  ghomfo  30381  exidreslem  32239  divrngcl  32260  isdrngo2  32261  dvbdfbdioolem1  37897  fourierdlem48  38130  fourierdlem49  38131  fourierdlem71  38153  fourierdlem73  38155  fourierdlem94  38176  fourierdlem111  38193  fourierdlem112  38194  fourierdlem113  38195  fouriersw  38207  fouriercn  38208  dmvon  38546  trlreslem  39895
  Copyright terms: Public domain W3C validator