Theorem dmres 6005

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 3454	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5885	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1986	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3454	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5980	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1881	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5885	. . . . . 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 4158	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2769	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ∩ cin 3898  ⟨cop 4590  dom cdm 5655   ↾ cres 5657

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5661  df-dm 5665  df-res 5667

This theorem is used by:  ssdmres  6006  dmresexg  6007  dmressnsn  6016  eldmeldmressn  6018  resindm  6023  relresdm1  6029  imadisj  6076  imainrect  6174  dmresv  6194  resdmres  6228  resdmss  6231  coeq0  6252  resssxp  6267  snres0  6296  funimacnv  6614  fnresdisj  6652  fnres  6659  fresaunres2  6747  nfvres  6916  ssimaex  6963  fnreseql  7040  respreima  7058  fveqressseq  7072  ffvresb  7119  fsnunfv  7185  funfvima  7229  funiunfv  7245  offres  7980  fnwelem  8129  ressuppss  8181  ressuppssdif  8183  frrlem11  8295  frrlem12  8296  smores  8341  smores3  8342  smores2  8343  tz7.44-2  8396  tz7.44-3  8397  frfnom  8424  sbthlem5  9089  sbthlem7  9091  domss2  9134  imafi  9285  ordtypelem4  9493  wdomima2g  9558  r0weon  10015  imadomg  10537  imadomnum  10538  dmaddpi  10899  dmmulpi  10900  ltweuz  14025  dmhashres  14405  limsupgle  15564  fvsetsid  17260  setsdm  17262  setsfun  17263  setsfun0  17264  setsres  17270  lubdm  18437  glbdm  18450  gsumzaddlem  20048  dprdcntz2  20167  lmres  23525  imacmp  23622  qtoptop2  23925  kqdisj  23958  metreslem  24588  setsmstopn  24704  ismbl  25754  mbfres  25872  dvres3a  26141  cpnres  26164  dvlipcn  26221  dvlip2  26222  c1lip3  26226  dvcnvrelem1  26244  dvcvx  26247  dvlog  26888  ltsres  27898  nolesgn2ores  27908  nogesgn1ores  27910  nodense  27928  nosupres  27943  nosupbnd1lem1  27944  nosupbnd2lem1  27951  nosupbnd2  27952  noinfres  27958  noinfbnd1lem1  27959  noinfbnd2lem1  27966  noetasuplem2  27970  noetainflem2  27974  oniso  28536  bdayn0sf1o  28635  uhgrspansubgrlem  29750  trlsegvdeglem4  30703  hlimcaui  31717  ftc2re  35106  dfrdg2  36372  bj-fvsnun2  38008  caures  38510  ssbnd  38538  dmcnvepres  39138  dmuncnvepres  39139  dmxrncnvepres2  39181  mapfzcons1  43562  diophrw  43604  eldioph2lem1  43605  eldioph2lem2  43606  tfsconcatrev  44189  limsupresxr  46594  liminfresxr  46595  fourierdlem93  47027  fouriersw  47059  eldmressn  47925  fnresfnco  47929  afvres  48060  afv2res  48127  resinsn  49798  resinsnALT  49799  tposrescnv  49805