Theorem dmres 6003

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 3455	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5883	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1986	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3455	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5978	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1881	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5883	. . . . . 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 2770	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

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

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 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5657  df-dm 5661  df-res 5663

This theorem is used by:  ssdmres  6004  dmresexg  6005  dmressnsn  6012  eldmeldmressn  6014  resindm  6019  relresdm1  6025  imadisj  6077  imainrect  6173  dmresv  6193  resdmres  6232  resdmss  6235  coeq0  6256  resssxp  6271  snres0  6300  funimacnv  6619  fnresdisj  6657  fnres  6664  fresaunres2  6752  nfvres  6921  ssimaex  6968  fnreseql  7045  respreima  7063  fveqressseq  7077  ffvresb  7124  fsnunfv  7190  funfvima  7234  funiunfv  7250  offres  7993  fnwelem  8141  ressuppss  8193  ressuppssdif  8195  frrlem11  8307  frrlem12  8308  smores  8353  smores3  8354  smores2  8355  tz7.44-2  8408  tz7.44-3  8409  frfnom  8436  sbthlem5  9103  sbthlem7  9105  domss2  9148  imafi  9300  ordtypelem4  9508  wdomima2g  9573  r0weon  10084  imadomg  10606  imadomnum  10607  dmaddpi  10968  dmmulpi  10969  ltweuz  14097  dmhashres  14478  limsupgle  15637  fvsetsid  17339  setsdm  17341  setsfun  17342  setsfun0  17343  setsres  17349  lubdm  18516  glbdm  18529  gsumzaddlem  20128  dprdcntz2  20247  lmres  23611  imacmp  23708  qtoptop2  24011  kqdisj  24044  metreslem  24674  setsmstopn  24790  ismbl  25840  mbfres  25958  dvres3a  26227  cpnres  26250  dvlipcn  26307  dvlip2  26308  c1lip3  26312  dvcnvrelem1  26330  dvcvx  26333  dvlog  26972  ltsres  28012  nolesgn2ores  28022  nogesgn1ores  28024  nodense  28042  nosupres  28057  nosupbnd1lem1  28058  nosupbnd2lem1  28065  nosupbnd2  28066  noinfres  28072  noinfbnd1lem1  28073  noinfbnd2lem1  28080  noetasuplem2  28084  noetainflem2  28088  oniso  28650  bdayn0sf1o  28749  uhgrspansubgrlem  29864  trlsegvdeglem4  30817  hlimcaui  31831  ftc2re  35220  dfrdg2  36537  bj-fvsnun2  38157  caures  38674  ssbnd  38702  dmcnvepres  39302  dmuncnvepres  39303  dmxrncnvepres2  39345  mapfzcons1  43707  diophrw  43749  eldioph2lem1  43750  eldioph2lem2  43751  tfsconcatrev  44334  limsupresxr  46745  liminfresxr  46746  fourierdlem93  47178  fouriersw  47210  eldmressn  48076  fnresfnco  48080  afvres  48211  afv2res  48278  resinsn  49949  resinsnALT  49950  tposrescnv  49956