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

Theorem dmres 5388
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 3193 . . . . 5 𝑥 ∈ V
21eldm2 5292 . . . 4 (𝑥 ∈ dom (𝐴𝐵) ↔ ∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵))
3 19.41v 1911 . . . . 5 (∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵) ↔ (∃𝑦𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
4 vex 3193 . . . . . . 7 𝑦 ∈ V
54opelres 5371 . . . . . 6 (⟨𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
65exbii 1771 . . . . 5 (∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ ∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
71eldm2 5292 . . . . . 6 (𝑥 ∈ dom 𝐴 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴)
87anbi1i 730 . . . . 5 ((𝑥 ∈ dom 𝐴𝑥𝐵) ↔ (∃𝑦𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
93, 6, 83bitr4i 292 . . . 4 (∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ (𝑥 ∈ dom 𝐴𝑥𝐵))
102, 9bitr2i 265 . . 3 ((𝑥 ∈ dom 𝐴𝑥𝐵) ↔ 𝑥 ∈ dom (𝐴𝐵))
1110ineqri 3790 . 2 (dom 𝐴𝐵) = dom (𝐴𝐵)
12 incom 3789 . 2 (dom 𝐴𝐵) = (𝐵 ∩ dom 𝐴)
1311, 12eqtr3i 2645 1 dom (𝐴𝐵) = (𝐵 ∩ dom 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1480  wex 1701  wcel 1987  cin 3559  cop 4161  dom cdm 5084  cres 5086
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-br 4624  df-opab 4684  df-xp 5090  df-dm 5094  df-res 5096
This theorem is referenced by:  ssdmres  5389  dmresexg  5390  dmressnsn  5407  eldmeldmressn  5409  imadisj  5453  imainrect  5544  dmresv  5562  resdmres  5594  coeq0  5613  funimacnv  5938  fnresdisj  5969  fnres  5975  fresaunres2  6043  nfvres  6191  ssimaex  6230  fnreseql  6293  respreima  6310  fveqressseq  6321  ffvresb  6360  fsnunfv  6418  funfvima  6457  funiunfv  6471  offres  7123  fnwelem  7252  ressuppss  7274  ressuppssdif  7276  smores  7409  smores3  7410  smores2  7411  tz7.44-2  7463  tz7.44-3  7464  frfnom  7490  sbthlem5  8034  sbthlem7  8036  domss2  8079  imafi  8219  ordtypelem4  8386  wdomima2g  8451  r0weon  8795  imadomg  9316  dmaddpi  9672  dmmulpi  9673  ltweuz  12716  dmhashres  13085  limsupgle  14158  fvsetsid  15830  setsdm  15832  setsfun  15833  setsfun0  15834  setsres  15841  lubdm  16919  glbdm  16932  gsumzaddlem  18261  dprdcntz2  18377  lmres  21044  imacmp  21140  qtoptop2  21442  kqdisj  21475  metreslem  22107  setsmstopn  22223  ismbl  23234  mbfres  23351  dvres3a  23618  cpnres  23640  dvlipcn  23695  dvlip2  23696  c1lip3  23700  dvcnvrelem1  23718  dvcvx  23721  dvlog  24331  uhgrspansubgrlem  26109  wlkres  26470  trlsegvdeglem4  26983  hlimcaui  27981  ftc2re  30492  dfrdg2  31455  sltres  31571  nodense  31605  nosires  31630  caures  33227  ssbnd  33258  mapfzcons1  36799  diophrw  36841  eldioph2lem1  36842  eldioph2lem2  36843  rp-imass  37586  dmresss  38946  fourierdlem93  39753  fouriersw  39785  sssmf  40284  eldmressn  40537  fnresfnco  40540  afvres  40586  setrec2lem1  41763
  Copyright terms: Public domain W3C validator