Theorem dmres 5911

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 3435	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5808	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1961	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3435	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5897	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1854	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5808	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi2i 623	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	3, 6, 8	3bitr4i 303	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴))
10	2, 9	bitr2i 275	. . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 4144	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2749	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 396   = wceq 1542  ∃wex 1786   ∈ wcel 2110   ∩ cin 3891  ⟨cop 4573  dom cdm 5589   ↾ cres 5591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-br 5080  df-opab 5142  df-xp 5595  df-dm 5599  df-res 5601

This theorem is referenced by:  ssdmres  5912  dmresexg  5913  dmressnsn  5931  eldmeldmressn  5933  imadisj  5986  imainrect  6082  dmresv  6101  resdmres  6133  resdmss  6136  coeq0  6157  resssxp  6171  funimacnv  6512  fnresdisj  6549  fnres  6556  fresaunres2  6643  nfvres  6805  ssimaex  6848  fnreseql  6920  respreima  6938  fveqressseq  6952  ffvresb  6993  fsnunfv  7054  funfvima  7101  funiunfv  7116  offres  7817  fnwelem  7961  ressuppss  7988  ressuppssdif  7990  frrlem11  8101  frrlem12  8102  smores  8172  smores3  8173  smores2  8174  tz7.44-2  8227  tz7.44-3  8228  frfnom  8255  sbthlem5  8854  sbthlem7  8856  domss2  8903  imafiALT  9088  ordtypelem4  9256  wdomima2g  9321  r0weon  9767  imadomg  10289  dmaddpi  10645  dmmulpi  10646  ltweuz  13677  dmhashres  14051  limsupgle  15182  fvsetsid  16865  setsdm  16867  setsfun  16868  setsfun0  16869  setsres  16875  lubdm  18065  glbdm  18078  gsumzaddlem  19518  dprdcntz2  19637  lmres  22447  imacmp  22544  qtoptop2  22846  kqdisj  22879  metreslem  23511  setsmstopn  23629  ismbl  24686  mbfres  24804  dvres3a  25074  cpnres  25097  dvlipcn  25154  dvlip2  25155  c1lip3  25159  dvcnvrelem1  25177  dvcvx  25180  dvlog  25802  uhgrspansubgrlem  27653  trlsegvdeglem4  28581  hlimcaui  29592  funresdm1  30938  ftc2re  32572  snres0  33669  dfrdg2  33765  sltres  33859  nolesgn2ores  33869  nogesgn1ores  33871  nodense  33889  nosupres  33904  nosupbnd1lem1  33905  nosupbnd2lem1  33912  nosupbnd2  33913  noinfres  33919  noinfbnd1lem1  33920  noinfbnd2lem1  33927  noetasuplem2  33931  noetainflem2  33935  bj-fvsnun2  35421  caures  35912  ssbnd  35940  mapfzcons1  40534  diophrw  40576  eldioph2lem1  40577  eldioph2lem2  40578  dmresss  42742  limsupresxr  43276  liminfresxr  43277  fourierdlem93  43709  fouriersw  43741  sssmf  44240  eldmressn  44497  fnresfnco  44501  afvres  44630  afv2res  44697