Theorem dmres 6020

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.

Step	Hyp	Ref	Expression
1		vex 3458	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5895	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1988	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3458	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5994	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1881	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5895	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi2i 635	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	3, 6, 8	3bitr4i 306	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴))
10	2, 9	bitr2i 279	. . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 4112	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2772	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2147   ∩ cin 4092  ⟨cop 4840  dom cdm 5658   ↾ cres 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-xp 5664  df-dm 5668  df-res 5670

This theorem is used by:  ssdmres  6021  dmresexg  6022  dmressnsn  6030  eldmeldmressn  6032  resindm  6037  relresdm1  6043  imadisj  6095  imainrect  6191  dmresv  6213  resdmres  6252  resdmss  6255  coeq0  6276  resssxp  6296  snres0  6327  funimacnv  6651  fnresdisj  6689  fnres  6696  fresaunres2  6784  nfvres  6954  ssimaex  7001  fnreseql  7078  respreima  7097  fveqressseq  7111  ffvresb  7158  fsnunfv  7223  funfvima  7267  funiunfv  7283  offres  8029  fnwelem  8180  ressuppss  8238  ressuppssdif  8240  frrlem11  8352  frrlem12  8353  smores  8398  smores3  8399  smores2  8400  tz7.44-2  8453  tz7.44-3  8454  frfnom  8481  sbthlem5  9148  sbthlem7  9150  domss2  9193  imafi  9345  ordtypelem4  9552  wdomima2g  9617  r0weon  10130  imadomg  10652  imadomnum  10653  dmaddpi  11014  dmmulpi  11015  ltweuz  14144  dmhashres  14526  limsupgle  15688  fvsetsid  17390  setsdm  17392  setsfun  17393  setsfun0  17394  setsres  17400  lubdm  18573  glbdm  18586  gsumzaddlem  20186  dprdcntz2  20305  lmres  23673  imacmp  23770  qtoptop2  24073  kqdisj  24106  metreslem  24736  setsmstopn  24852  ismbl  25902  mbfres  26020  dvres3a  26289  cpnres  26312  dvlipcn  26369  dvlip2  26370  c1lip3  26374  dvcnvrelem1  26392  dvcvx  26395  dvlog  27036  ltsres  28076  nolesgn2ores  28086  nogesgn1ores  28088  nodense  28106  nosupres  28121  nosupbnd1lem1  28122  nosupbnd2lem1  28129  nosupbnd2  28130  noinfres  28136  noinfbnd1lem1  28137  noinfbnd2lem1  28144  noetasuplem2  28148  noetainflem2  28152  oniso  28714  bdayn0sf1o  28813  uhgrspansubgrlem  29928  trlsegvdeglem4  30881  hlimcaui  31895  ftc2re  35338  fwfffunres  35829  dfrdg2  36772  cossididres  38224  nvo3  38230  bj-fvsnun2  38445  caures  38960  ssbnd  38988  dmcnvepres  39588  dmuncnvepres  39589  dmxrncnvepres2  39631  mapfzcons1  43994  diophrw  44036  eldioph2lem1  44037  eldioph2lem2  44038  tfsconcatrev  44611  limsupresxr  47049  liminfresxr  47050  fourierdlem93  47482  fouriersw  47514  eldmressn  48380  fnresfnco  48384  afvres  48515  afv2res  48582  resinsn  50316  resinsnALT  50317  tposrescnv  50323