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

Theorem dmres 5454
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 3234 . . . . 5 𝑥 ∈ V
21eldm2 5354 . . . 4 (𝑥 ∈ dom (𝐴𝐵) ↔ ∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵))
3 19.41v 1917 . . . . 5 (∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵) ↔ (∃𝑦𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
4 vex 3234 . . . . . . 7 𝑦 ∈ V
54opelres 5436 . . . . . 6 (⟨𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
65exbii 1814 . . . . 5 (∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ ∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
71eldm2 5354 . . . . . 6 (𝑥 ∈ dom 𝐴 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴)
87anbi1i 731 . . . . 5 ((𝑥 ∈ dom 𝐴𝑥𝐵) ↔ (∃𝑦𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
93, 6, 83bitr4i 292 . . . 4 (∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ (𝑥 ∈ dom 𝐴𝑥𝐵))
102, 9bitr2i 265 . . 3 ((𝑥 ∈ dom 𝐴𝑥𝐵) ↔ 𝑥 ∈ dom (𝐴𝐵))
1110ineqri 3839 . 2 (dom 𝐴𝐵) = dom (𝐴𝐵)
12 incom 3838 . 2 (dom 𝐴𝐵) = (𝐵 ∩ dom 𝐴)
1311, 12eqtr3i 2675 1 dom (𝐴𝐵) = (𝐵 ∩ dom 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1523  wex 1744  wcel 2030  cin 3606  cop 4216  dom cdm 5143  cres 5145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-xp 5149  df-dm 5153  df-res 5155
This theorem is referenced by:  ssdmres  5455  dmresexg  5456  dmressnsn  5473  eldmeldmressn  5475  imadisj  5519  imainrect  5610  dmresv  5628  resdmres  5663  coeq0  5682  funimacnv  6008  fnresdisj  6039  fnres  6045  fresaunres2  6114  nfvres  6262  ssimaex  6302  fnreseql  6367  respreima  6384  fveqressseq  6395  ffvresb  6434  fsnunfv  6494  funfvima  6532  funiunfv  6546  offres  7205  fnwelem  7337  ressuppss  7359  ressuppssdif  7361  smores  7494  smores3  7495  smores2  7496  tz7.44-2  7548  tz7.44-3  7549  frfnom  7575  sbthlem5  8115  sbthlem7  8117  domss2  8160  imafi  8300  ordtypelem4  8467  wdomima2g  8532  r0weon  8873  imadomg  9394  dmaddpi  9750  dmmulpi  9751  ltweuz  12800  dmhashres  13169  limsupgle  14252  fvsetsid  15937  setsdm  15939  setsfun  15940  setsfun0  15941  setsres  15948  lubdm  17026  glbdm  17039  gsumzaddlem  18367  dprdcntz2  18483  lmres  21152  imacmp  21248  qtoptop2  21550  kqdisj  21583  metreslem  22214  setsmstopn  22330  ismbl  23340  mbfres  23456  dvres3a  23723  cpnres  23745  dvlipcn  23802  dvlip2  23803  c1lip3  23807  dvcnvrelem1  23825  dvcvx  23828  dvlog  24442  uhgrspansubgrlem  26227  wlkres  26623  trlsegvdeglem4  27201  hlimcaui  28221  funresdm1  29542  ftc2re  30804  dfrdg2  31825  sltres  31940  nolesgn2ores  31950  nodense  31967  nosupres  31978  nosupbnd1lem1  31979  nosupbnd2lem1  31986  nosupbnd2  31987  caures  33686  ssbnd  33717  mapfzcons1  37597  diophrw  37639  eldioph2lem1  37640  eldioph2lem2  37641  rp-imass  38382  dmresss  39750  limsupresxr  40316  liminfresxr  40317  fourierdlem93  40734  fouriersw  40766  sssmf  41268  eldmressn  41524  fnresfnco  41527  afvres  41573  setrec2lem1  42765
  Copyright terms: Public domain W3C validator