Theorem dmres 6004

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 3479	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5902	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1958	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3479	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5990	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1851	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5902	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi2i 624	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	3, 6, 8	3bitr4i 303	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴))
10	2, 9	bitr2i 276	. . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 4205	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2742	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 397   = wceq 1542  ∃wex 1782   ∈ wcel 2107   ∩ cin 3948  ⟨cop 4635  dom cdm 5677   ↾ cres 5679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-xp 5683  df-dm 5687  df-res 5689

This theorem is referenced by:  ssdmres  6005  dmresexg  6006  dmressnsn  6024  eldmeldmressn  6026  relresdm1  6034  imadisj  6080  imainrect  6181  dmresv  6200  resdmres  6232  resdmss  6235  coeq0  6255  resssxp  6270  snres0  6298  funimacnv  6630  fnresdisj  6671  fnres  6678  fresaunres2  6764  nfvres  6933  ssimaex  6977  fnreseql  7050  respreima  7068  fveqressseq  7082  ffvresb  7124  fsnunfv  7185  funfvima  7232  funiunfv  7247  offres  7970  fnwelem  8117  ressuppss  8168  ressuppssdif  8170  frrlem11  8281  frrlem12  8282  smores  8352  smores3  8353  smores2  8354  tz7.44-2  8407  tz7.44-3  8408  frfnom  8435  sbthlem5  9087  sbthlem7  9089  domss2  9136  imafiALT  9345  ordtypelem4  9516  wdomima2g  9581  r0weon  10007  imadomg  10529  dmaddpi  10885  dmmulpi  10886  ltweuz  13926  dmhashres  14301  limsupgle  15421  fvsetsid  17101  setsdm  17103  setsfun  17104  setsfun0  17105  setsres  17111  lubdm  18304  glbdm  18317  gsumzaddlem  19789  dprdcntz2  19908  lmres  22804  imacmp  22901  qtoptop2  23203  kqdisj  23236  metreslem  23868  setsmstopn  23986  ismbl  25043  mbfres  25161  dvres3a  25431  cpnres  25454  dvlipcn  25511  dvlip2  25512  c1lip3  25516  dvcnvrelem1  25534  dvcvx  25537  dvlog  26159  sltres  27165  nolesgn2ores  27175  nogesgn1ores  27177  nodense  27195  nosupres  27210  nosupbnd1lem1  27211  nosupbnd2lem1  27218  nosupbnd2  27219  noinfres  27225  noinfbnd1lem1  27226  noinfbnd2lem1  27233  noetasuplem2  27237  noetainflem2  27241  uhgrspansubgrlem  28547  trlsegvdeglem4  29476  hlimcaui  30489  ftc2re  33610  dfrdg2  34767  bj-fvsnun2  36137  caures  36628  ssbnd  36656  mapfzcons1  41455  diophrw  41497  eldioph2lem1  41498  eldioph2lem2  41499  tfsconcatrev  42098  dmresss  43933  limsupresxr  44482  liminfresxr  44483  fourierdlem93  44915  fouriersw  44947  sssmf  45454  eldmressn  45747  fnresfnco  45751  afvres  45880  afv2res  45947