Theorem dmres 5965

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 3441	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5845	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1954	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3441	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5940	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1849	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5845	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi2i 623	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	3, 6, 8	3bitr4i 303	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴))
10	2, 9	bitr2i 276	. . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 4161	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2742	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113   ∩ cin 3897  ⟨cop 4581  dom cdm 5619   ↾ cres 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-xp 5625  df-dm 5629  df-res 5631

This theorem is referenced by:  ssdmres  5966  dmresexg  5967  dmressnsn  5976  eldmeldmressn  5978  relresdm1  5986  imadisj  6033  imainrect  6133  dmresv  6152  resdmres  6184  resdmss  6187  coeq0  6208  resssxp  6222  snres0  6250  funimacnv  6567  fnresdisj  6606  fnres  6613  fresaunres2  6700  nfvres  6866  ssimaex  6913  fnreseql  6987  respreima  7005  fveqressseq  7018  ffvresb  7064  fsnunfv  7127  funfvima  7170  funiunfv  7188  offres  7921  fnwelem  8067  ressuppss  8119  ressuppssdif  8121  frrlem11  8232  frrlem12  8233  smores  8278  smores3  8279  smores2  8280  tz7.44-2  8332  tz7.44-3  8333  frfnom  8360  sbthlem5  9011  sbthlem7  9013  domss2  9056  imafi  9206  ordtypelem4  9414  wdomima2g  9479  r0weon  9910  imadomg  10432  dmaddpi  10788  dmmulpi  10789  ltweuz  13870  dmhashres  14250  limsupgle  15386  fvsetsid  17081  setsdm  17083  setsfun  17084  setsfun0  17085  setsres  17091  lubdm  18257  glbdm  18270  gsumzaddlem  19835  dprdcntz2  19954  lmres  23216  imacmp  23313  qtoptop2  23615  kqdisj  23648  metreslem  24278  setsmstopn  24394  ismbl  25455  mbfres  25573  dvres3a  25843  cpnres  25867  dvlipcn  25927  dvlip2  25928  c1lip3  25932  dvcnvrelem1  25950  dvcvx  25953  dvlog  26588  sltres  27602  nolesgn2ores  27612  nogesgn1ores  27614  nodense  27632  nosupres  27647  nosupbnd1lem1  27648  nosupbnd2lem1  27655  nosupbnd2  27656  noinfres  27662  noinfbnd1lem1  27663  noinfbnd2lem1  27670  noetasuplem2  27674  noetainflem2  27678  onsiso  28206  bdayn0sf1o  28296  uhgrspansubgrlem  29270  trlsegvdeglem4  30205  hlimcaui  31218  ftc2re  34632  dfrdg2  35858  bj-fvsnun2  37321  caures  37820  ssbnd  37848  dmcnvepres  38434  dmuncnvepres  38435  dmxrncnvepres2  38477  mapfzcons1  42834  diophrw  42876  eldioph2lem1  42877  eldioph2lem2  42878  tfsconcatrev  43465  limsupresxr  45888  liminfresxr  45889  fourierdlem93  46321  fouriersw  46353  sssmf  46860  eldmressn  47161  fnresfnco  47165  afvres  47296  afv2res  47363  resinsn  48996  resinsnALT  48997  tposrescnv  49003