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

Theorem dmres 5668
Description: The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
dmres dom (𝐴𝐵) = (𝐵 ∩ dom 𝐴)

Proof of Theorem dmres
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3401 . . . . 5 𝑥 ∈ V
21eldm2 5567 . . . 4 (𝑥 ∈ dom (𝐴𝐵) ↔ ∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵))
3 19.42v 1996 . . . . 5 (∃𝑦(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥𝐵 ∧ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴))
4 vex 3401 . . . . . . 7 𝑦 ∈ V
54opelresi 5650 . . . . . 6 (⟨𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ (𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
65exbii 1892 . . . . 5 (∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ ∃𝑦(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
71eldm2 5567 . . . . . 6 (𝑥 ∈ dom 𝐴 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴)
87anbi2i 616 . . . . 5 ((𝑥𝐵𝑥 ∈ dom 𝐴) ↔ (𝑥𝐵 ∧ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴))
93, 6, 83bitr4i 295 . . . 4 (∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ (𝑥𝐵𝑥 ∈ dom 𝐴))
102, 9bitr2i 268 . . 3 ((𝑥𝐵𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴𝐵))
1110ineqri 4029 . 2 (𝐵 ∩ dom 𝐴) = dom (𝐴𝐵)
1211eqcomi 2787 1 dom (𝐴𝐵) = (𝐵 ∩ dom 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wa 386   = wceq 1601  wex 1823  wcel 2107  cin 3791  cop 4404  dom cdm 5355  cres 5357
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pr 5138
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4887  df-opab 4949  df-xp 5361  df-dm 5365  df-res 5367
This theorem is referenced by:  ssdmres  5669  dmresexg  5670  dmressnsn  5688  eldmeldmressn  5690  imadisj  5738  imainrect  5829  dmresv  5847  resdmres  5879  coeq0  5898  funimacnv  6215  fnresdisj  6247  fnres  6253  fresaunres2  6326  nfvres  6483  ssimaex  6523  fnreseql  6590  respreima  6608  fveqressseq  6619  ffvresb  6658  fsnunfv  6724  funfvima  6764  funiunfv  6778  offres  7440  fnwelem  7573  ressuppss  7595  ressuppssdif  7597  smores  7732  smores3  7733  smores2  7734  tz7.44-2  7786  tz7.44-3  7787  frfnom  7813  sbthlem5  8362  sbthlem7  8364  domss2  8407  imafi  8547  ordtypelem4  8715  wdomima2g  8780  r0weon  9168  imadomg  9691  dmaddpi  10047  dmmulpi  10048  ltweuz  13079  dmhashres  13446  limsupgle  14616  fvsetsid  16287  setsdm  16289  setsfun  16290  setsfun0  16291  setsres  16297  lubdm  17365  glbdm  17378  gsumzaddlem  18707  dprdcntz2  18824  lmres  21512  imacmp  21609  qtoptop2  21911  kqdisj  21944  metreslem  22575  setsmstopn  22691  ismbl  23730  mbfres  23848  dvres3a  24115  cpnres  24137  dvlipcn  24194  dvlip2  24195  c1lip3  24199  dvcnvrelem1  24217  dvcvx  24220  dvlog  24834  uhgrspansubgrlem  26637  wlkresOLD  27021  trlsegvdeglem4  27627  hlimcaui  28665  funresdm1  29979  ftc2re  31278  dfrdg2  32289  sltres  32404  nolesgn2ores  32414  nodense  32431  nosupres  32442  nosupbnd1lem1  32443  nosupbnd2lem1  32450  nosupbnd2  32451  bj-fvsnun2  33734  caures  34182  ssbnd  34213  mapfzcons1  38244  diophrw  38286  eldioph2lem1  38287  eldioph2lem2  38288  rp-imass  39025  dmresss  40357  limsupresxr  40910  liminfresxr  40911  fourierdlem93  41347  fouriersw  41379  sssmf  41878  eldmressn  42105  fnresfnco  42109  afvres  42217  afv2res  42284  setrec2lem1  43549
  Copyright terms: Public domain W3C validator