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

Theorem dmres 5844
 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 3447 . . . . 5 𝑥 ∈ V
21eldm2 5738 . . . 4 (𝑥 ∈ dom (𝐴𝐵) ↔ ∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵))
3 19.42v 1954 . . . . 5 (∃𝑦(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥𝐵 ∧ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴))
4 vex 3447 . . . . . . 7 𝑦 ∈ V
54opelresi 5830 . . . . . 6 (⟨𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ (𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
65exbii 1849 . . . . 5 (∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ ∃𝑦(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
71eldm2 5738 . . . . . 6 (𝑥 ∈ dom 𝐴 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴)
87anbi2i 625 . . . . 5 ((𝑥𝐵𝑥 ∈ dom 𝐴) ↔ (𝑥𝐵 ∧ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴))
93, 6, 83bitr4i 306 . . . 4 (∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ (𝑥𝐵𝑥 ∈ dom 𝐴))
102, 9bitr2i 279 . . 3 ((𝑥𝐵𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴𝐵))
1110ineqri 4133 . 2 (𝐵 ∩ dom 𝐴) = dom (𝐴𝐵)
1211eqcomi 2810 1 dom (𝐴𝐵) = (𝐵 ∩ dom 𝐴)
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2112   ∩ cin 3883  ⟨cop 4534  dom cdm 5523   ↾ cres 5525 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-xp 5529  df-dm 5533  df-res 5535 This theorem is referenced by:  ssdmres  5845  dmresexg  5846  dmressnsn  5864  eldmeldmressn  5866  imadisj  5919  imainrect  6009  dmresv  6028  resdmres  6060  coeq0  6079  resssxp  6093  funimacnv  6409  fnresdisj  6443  fnres  6450  fresaunres2  6528  nfvres  6685  ssimaex  6727  fnreseql  6799  respreima  6817  fveqressseq  6828  ffvresb  6869  fsnunfv  6930  funfvima  6974  funiunfv  6989  offres  7670  fnwelem  7812  ressuppss  7836  ressuppssdif  7838  smores  7976  smores3  7977  smores2  7978  tz7.44-2  8030  tz7.44-3  8031  frfnom  8057  sbthlem5  8619  sbthlem7  8621  domss2  8664  imafi  8805  ordtypelem4  8973  wdomima2g  9038  r0weon  9427  imadomg  9949  dmaddpi  10305  dmmulpi  10306  ltweuz  13328  dmhashres  13701  limsupgle  14830  fvsetsid  16511  setsdm  16513  setsfun  16514  setsfun0  16515  setsres  16521  lubdm  17585  glbdm  17598  gsumzaddlem  19038  dprdcntz2  19157  lmres  21909  imacmp  22006  qtoptop2  22308  kqdisj  22341  metreslem  22973  setsmstopn  23089  ismbl  24134  mbfres  24252  dvres3a  24521  cpnres  24544  dvlipcn  24601  dvlip2  24602  c1lip3  24606  dvcnvrelem1  24624  dvcvx  24627  dvlog  25246  uhgrspansubgrlem  27084  trlsegvdeglem4  28012  hlimcaui  29023  funresdm1  30372  ftc2re  31983  dfrdg2  33154  frrlem11  33247  frrlem12  33248  sltres  33283  nolesgn2ores  33293  nodense  33310  nosupres  33321  nosupbnd1lem1  33322  nosupbnd2lem1  33329  nosupbnd2  33330  bj-fvsnun2  34672  caures  35197  ssbnd  35225  mapfzcons1  39651  diophrw  39693  eldioph2lem1  39694  eldioph2lem2  39695  dmresss  41860  limsupresxr  42401  liminfresxr  42402  fourierdlem93  42834  fouriersw  42866  sssmf  43365  eldmressn  43622  fnresfnco  43626  afvres  43721  afv2res  43788
 Copyright terms: Public domain W3C validator