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

Theorem dmres 5323
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 3172 . . . . 5 𝑥 ∈ V
21eldm2 5228 . . . 4 (𝑥 ∈ dom (𝐴𝐵) ↔ ∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵))
3 19.41v 1900 . . . . 5 (∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵) ↔ (∃𝑦𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
4 vex 3172 . . . . . . 7 𝑦 ∈ V
54opelres 5306 . . . . . 6 (⟨𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
65exbii 1763 . . . . 5 (∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ ∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
71eldm2 5228 . . . . . 6 (𝑥 ∈ dom 𝐴 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴)
87anbi1i 726 . . . . 5 ((𝑥 ∈ dom 𝐴𝑥𝐵) ↔ (∃𝑦𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
93, 6, 83bitr4i 290 . . . 4 (∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ (𝑥 ∈ dom 𝐴𝑥𝐵))
102, 9bitr2i 263 . . 3 ((𝑥 ∈ dom 𝐴𝑥𝐵) ↔ 𝑥 ∈ dom (𝐴𝐵))
1110ineqri 3764 . 2 (dom 𝐴𝐵) = dom (𝐴𝐵)
12 incom 3763 . 2 (dom 𝐴𝐵) = (𝐵 ∩ dom 𝐴)
1311, 12eqtr3i 2630 1 dom (𝐴𝐵) = (𝐵 ∩ dom 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wa 382   = wceq 1474  wex 1694  wcel 1976  cin 3535  cop 4127  dom cdm 5025  cres 5027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pr 4825
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-br 4575  df-opab 4635  df-xp 5031  df-dm 5035  df-res 5037
This theorem is referenced by:  ssdmres  5324  dmresexg  5325  dmressnsn  5342  eldmeldmressn  5344  imadisj  5387  imainrect  5477  dmresv  5494  resdmres  5526  coeq0  5544  funimacnv  5867  fnresdisj  5898  fnres  5904  fresaunres2  5971  nfvres  6116  ssimaex  6155  fnreseql  6217  respreima  6234  fveqressseq  6245  ffvresb  6283  fsnunfv  6333  funfvima  6371  funiunfv  6385  offres  7028  fnwelem  7153  ressuppss  7175  ressuppssdif  7177  smores  7310  smores3  7311  smores2  7312  tz7.44-2  7364  tz7.44-3  7365  frfnom  7391  sbthlem5  7933  sbthlem7  7935  domss2  7978  imafi  8116  ordtypelem4  8283  wdomima2g  8348  r0weon  8692  imadomg  9211  dmaddpi  9565  dmmulpi  9566  ltweuz  12574  dmhashres  12940  limsupgle  13999  fvsetsid  15665  setsdm  15667  setsfun  15668  setsfun0  15669  setsres  15672  lubdm  16745  glbdm  16758  gsumzaddlem  18087  dprdcntz2  18203  lmres  20853  imacmp  20949  qtoptop2  21251  kqdisj  21284  metreslem  21915  setsmstopn  22031  ismbl  23015  mbfres  23131  dvres3a  23398  cpnres  23420  dvlipcn  23475  dvlip2  23476  c1lip3  23480  dvcnvrelem1  23498  dvcvx  23501  dvlog  24111  cusgrasizeindslem1  25765  eupares  26265  hlimcaui  27280  dfrdg2  30748  sltres  30864  nodense  30891  nofulllem5  30908  caures  32526  ssbnd  32557  mapfzcons1  36098  diophrw  36140  eldioph2lem1  36141  eldioph2lem2  36142  rp-imass  36885  fourierdlem93  38893  fouriersw  38925  sssmf  39426  eldmressn  39653  fnresfnco  39656  afvres  39703  uhgrspansubgrlem  40513  1wlkres  40878  trlsegvdeglem4  41390
  Copyright terms: Public domain W3C validator