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

Theorem dmres 5153
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
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2946 . . . . 5  |-  x  e. 
_V
21eldm2 5054 . . . 4  |-  ( x  e.  dom  ( A  |`  B )  <->  E. y <. x ,  y >.  e.  ( A  |`  B ) )
3 19.41v 1924 . . . . 5  |-  ( E. y ( <. x ,  y >.  e.  A  /\  x  e.  B
)  <->  ( E. y <. x ,  y >.  e.  A  /\  x  e.  B ) )
4 vex 2946 . . . . . . 7  |-  y  e. 
_V
54opelres 5137 . . . . . 6  |-  ( <.
x ,  y >.  e.  ( A  |`  B )  <-> 
( <. x ,  y
>.  e.  A  /\  x  e.  B ) )
65exbii 1592 . . . . 5  |-  ( E. y <. x ,  y
>.  e.  ( A  |`  B )  <->  E. y
( <. x ,  y
>.  e.  A  /\  x  e.  B ) )
71eldm2 5054 . . . . . 6  |-  ( x  e.  dom  A  <->  E. y <. x ,  y >.  e.  A )
87anbi1i 677 . . . . 5  |-  ( ( x  e.  dom  A  /\  x  e.  B
)  <->  ( E. y <. x ,  y >.  e.  A  /\  x  e.  B ) )
93, 6, 83bitr4i 269 . . . 4  |-  ( E. y <. x ,  y
>.  e.  ( A  |`  B )  <->  ( x  e.  dom  A  /\  x  e.  B ) )
102, 9bitr2i 242 . . 3  |-  ( ( x  e.  dom  A  /\  x  e.  B
)  <->  x  e.  dom  ( A  |`  B ) )
1110ineqri 3521 . 2  |-  ( dom 
A  i^i  B )  =  dom  ( A  |`  B )
12 incom 3520 . 2  |-  ( dom 
A  i^i  B )  =  ( B  i^i  dom 
A )
1311, 12eqtr3i 2452 1  |-  dom  ( A  |`  B )  =  ( B  i^i  dom  A )
Colors of variables: wff set class
Syntax hints:    /\ wa 359   E.wex 1550    = wceq 1652    e. wcel 1725    i^i cin 3306   <.cop 3804   dom cdm 4864    |` cres 4866
This theorem is referenced by:  ssdmres  5154  dmresexg  5155  imadisj  5209  ndmima  5227  imainrect  5298  dmresv  5315  resdmres  5347  funimacnv  5511  fnresdisj  5541  fnres  5547  fresaunres2  5601  nfvres  5746  ssimaex  5774  fnreseql  5826  respreima  5845  ffvresb  5886  fsnunfv  5919  funfvima  5959  funiunfv  5981  offres  6305  fnwelem  6447  smores  6600  smores3  6601  smores2  6602  tz7.44-2  6651  tz7.44-3  6652  frfnom  6678  sbthlem5  7207  sbthlem7  7209  domss2  7252  imafi  7385  ordtypelem4  7474  wdomima2g  7538  r0weon  7878  imadomg  8396  dmaddpi  8751  dmmulpi  8752  ltweuz  11284  limsupgle  12254  setsres  13478  gsumzaddlem  15509  dprdcntz2  15579  lmres  17347  imacmp  17443  qtoptop2  17714  kqdisj  17747  metreslem  18375  setsmstopn  18491  ismbl  19405  mbfres  19519  dvres3a  19784  cpnres  19806  dvlipcn  19861  dvlip2  19862  c1lip3  19866  dvcnvrelem1  19884  dvcvx  19887  dvlog  20525  cusgrasizeindslem2  21466  eupares  21680  hlimcaui  22722  dmhashres  24140  dfrdg2  25402  sltres  25568  nodense  25593  nofulllem5  25610  caures  26398  ssbnd  26429  mapfzcons1  26705  coeq0  26742  diophrw  26749  eldioph2lem1  26750  eldioph2lem2  26751  eldmressn  27893  dmressnsn  27894  fnresfnco  27899  afvres  27945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411  ax-sep 4317  ax-nul 4325  ax-pr 4390
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ne 2595  df-ral 2697  df-rex 2698  df-rab 2701  df-v 2945  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-nul 3616  df-if 3727  df-sn 3807  df-pr 3808  df-op 3810  df-br 4200  df-opab 4254  df-xp 4870  df-dm 4874  df-res 4876
  Copyright terms: Public domain W3C validator