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

Theorem dmres 5616
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 3390 . . . . 5 𝑥 ∈ V
21eldm2 5517 . . . 4 (𝑥 ∈ dom (𝐴𝐵) ↔ ∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵))
3 19.41v 2039 . . . . 5 (∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵) ↔ (∃𝑦𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
4 vex 3390 . . . . . . 7 𝑦 ∈ V
54opelres 5599 . . . . . 6 (⟨𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
65exbii 1933 . . . . 5 (∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ ∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
71eldm2 5517 . . . . . 6 (𝑥 ∈ dom 𝐴 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴)
87anbi1i 612 . . . . 5 ((𝑥 ∈ dom 𝐴𝑥𝐵) ↔ (∃𝑦𝑥, 𝑦⟩ ∈ 𝐴𝑥𝐵))
93, 6, 83bitr4i 294 . . . 4 (∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ (𝑥 ∈ dom 𝐴𝑥𝐵))
102, 9bitr2i 267 . . 3 ((𝑥 ∈ dom 𝐴𝑥𝐵) ↔ 𝑥 ∈ dom (𝐴𝐵))
1110ineqri 3999 . 2 (dom 𝐴𝐵) = dom (𝐴𝐵)
12 incom 3998 . 2 (dom 𝐴𝐵) = (𝐵 ∩ dom 𝐴)
1311, 12eqtr3i 2826 1 dom (𝐴𝐵) = (𝐵 ∩ dom 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1637  wex 1859  wcel 2155  cin 3762  cop 4370  dom cdm 5305  cres 5307
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968  ax-nul 4977  ax-pr 5090
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ral 3097  df-rex 3098  df-rab 3101  df-v 3389  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-nul 4111  df-if 4274  df-sn 4365  df-pr 4367  df-op 4371  df-br 4838  df-opab 4900  df-xp 5311  df-dm 5315  df-res 5317
This theorem is referenced by:  ssdmres  5617  dmresexg  5618  dmressnsn  5637  eldmeldmressn  5639  imadisj  5688  imainrect  5780  dmresv  5798  resdmres  5833  coeq0  5852  funimacnv  6175  fnresdisj  6206  fnres  6212  fresaunres2  6285  nfvres  6438  ssimaex  6478  fnreseql  6543  respreima  6560  fveqressseq  6571  ffvresb  6610  fsnunfv  6672  funfvima  6711  funiunfv  6724  offres  7387  fnwelem  7520  ressuppss  7542  ressuppssdif  7544  smores  7679  smores3  7680  smores2  7681  tz7.44-2  7733  tz7.44-3  7734  frfnom  7760  sbthlem5  8307  sbthlem7  8309  domss2  8352  imafi  8492  ordtypelem4  8659  wdomima2g  8724  r0weon  9112  imadomg  9635  dmaddpi  9991  dmmulpi  9992  ltweuz  12978  dmhashres  13343  limsupgle  14425  fvsetsid  16095  setsdm  16097  setsfun  16098  setsfun0  16099  setsres  16106  lubdm  17178  glbdm  17191  gsumzaddlem  18516  dprdcntz2  18633  lmres  21312  imacmp  21408  qtoptop2  21710  kqdisj  21743  metreslem  22374  setsmstopn  22490  ismbl  23501  mbfres  23619  dvres3a  23886  cpnres  23908  dvlipcn  23965  dvlip2  23966  c1lip3  23970  dvcnvrelem1  23988  dvcvx  23991  dvlog  24605  uhgrspansubgrlem  26392  wlkres  26789  trlsegvdeglem4  27390  hlimcaui  28415  funresdm1  29735  ftc2re  30995  dfrdg2  32015  sltres  32130  nolesgn2ores  32140  nodense  32157  nosupres  32168  nosupbnd1lem1  32169  nosupbnd2lem1  32176  nosupbnd2  32177  caures  33861  ssbnd  33892  mapfzcons1  37776  diophrw  37818  eldioph2lem1  37819  eldioph2lem2  37820  rp-imass  38559  dmresss  39914  limsupresxr  40472  liminfresxr  40473  fourierdlem93  40889  fouriersw  40921  sssmf  41423  eldmressn  41650  fnresfnco  41654  afvres  41755  afv2res  41822  setrec2lem1  43002
  Copyright terms: Public domain W3C validator