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

Theorem dmres 4975
Description: The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
dmres  |-  dom  (  A  |`  B )  =  ( B  i^i  dom  A )

Proof of Theorem dmres
StepHypRef Expression
1 vex 2792 . . . . 5  |-  x  e. 
_V
21eldm2 4876 . . . 4  |-  ( x  e.  dom  (  A  |`  B )  <->  E. y <. x ,  y >.  e.  ( A  |`  B ) )
3 19.41v 1853 . . . . 5  |-  ( E. y ( <. x ,  y >.  e.  A  /\  x  e.  B
)  <->  ( E. y <. x ,  y >.  e.  A  /\  x  e.  B ) )
4 vex 2792 . . . . . . 7  |-  y  e. 
_V
54opelres 4959 . . . . . 6  |-  ( <.
x ,  y >.  e.  ( A  |`  B )  <-> 
( <. x ,  y
>.  e.  A  /\  x  e.  B ) )
65exbii 1574 . . . . 5  |-  ( E. y <. x ,  y
>.  e.  ( A  |`  B )  <->  E. y
( <. x ,  y
>.  e.  A  /\  x  e.  B ) )
71eldm2 4876 . . . . . 6  |-  ( x  e.  dom  A  <->  E. y <. x ,  y >.  e.  A )
87anbi1i 679 . . . . 5  |-  ( ( x  e.  dom  A  /\  x  e.  B
)  <->  ( E. y <. x ,  y >.  e.  A  /\  x  e.  B ) )
93, 6, 83bitr4i 270 . . . 4  |-  ( E. y <. x ,  y
>.  e.  ( A  |`  B )  <->  ( x  e.  dom  A  /\  x  e.  B ) )
102, 9bitr2i 243 . . 3  |-  ( ( x  e.  dom  A  /\  x  e.  B
)  <->  x  e.  dom  (  A  |`  B ) )
1110ineqri 3363 . 2  |-  ( dom 
A  i^i  B )  =  dom  (  A  |`  B )
12 incom 3362 . 2  |-  ( dom 
A  i^i  B )  =  ( B  i^i  dom 
A )
1311, 12eqtr3i 2306 1  |-  dom  (  A  |`  B )  =  ( B  i^i  dom  A )
Colors of variables: wff set class
Syntax hints:    /\ wa 360   E.wex 1533    = wceq 1628    e. wcel 1688    i^i cin 3152   <.cop 3644   dom cdm 4688    |` cres 4690
This theorem is referenced by:  ssdmres  4976  dmresexg  4977  imadisj  5031  ndmima  5049  imainrect  5118  dmresv  5130  resdmres  5162  funimacnv  5289  fnresdisj  5319  fnres  5325  fresaunres2  5378  nfvres  5518  ssimaex  5545  fnreseql  5596  respreima  5615  ffvresb  5651  fsnunfv  5681  funfvima  5714  funiunfv  5735  offres  6053  fnwelem  6191  smores  6364  smores3  6365  smores2  6366  tz7.44-2  6415  tz7.44-3  6416  frfnom  6442  sbthlem5  6970  sbthlem7  6972  domss2  7015  imafi  7143  ordtypelem4  7231  wdomima2g  7295  r0weon  7635  imadomg  8154  dmaddpi  8509  dmmulpi  8510  ltweuz  11018  limsupgle  11945  setsres  13168  gsumzaddlem  15197  dprdcntz2  15267  lmres  17022  imacmp  17118  qtoptop2  17384  kqdisj  17417  metreslem  17920  setsmstopn  18018  ismbl  18879  mbfres  18993  dvres3a  19258  cpnres  19280  dvlipcn  19335  dvlip2  19336  c1lip3  19340  dvcnvrelem1  19358  dvcvx  19361  dvlog  19992  hlimcaui  21808  eupares  23303  dfrdg2  23553  sltres  23718  axdense  23744  axfelem18  23764  caures  25875  ssbnd  25911  mapfzcons1  26193  coeq0  26230  diophrw  26237  eldioph2lem1  26238  eldioph2lem2  26239  eldmressn  27355  dmressnsn  27356  fnresfnco  27362  funcoressn  27363  funressnfv  27364  afvres  27411
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-14 1692  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-br 4025  df-opab 4079  df-xp 4694  df-dm 4698  df-res 4700
  Copyright terms: Public domain W3C validator