Theorem dmres 6030

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 3484	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5912	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1953	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3484	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 6005	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1848	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5912	. . . . . 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 4212	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2746	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2108   ∩ cin 3950  ⟨cop 4632  dom cdm 5685   ↾ cres 5687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-dm 5695  df-res 5697

This theorem is referenced by:  ssdmres  6031  dmresexg  6032  dmressnsn  6041  eldmeldmressn  6043  relresdm1  6051  imadisj  6098  imainrect  6201  dmresv  6220  resdmres  6252  resdmss  6255  coeq0  6275  resssxp  6290  snres0  6318  funimacnv  6647  fnresdisj  6688  fnres  6695  fresaunres2  6780  nfvres  6947  ssimaex  6994  fnreseql  7068  respreima  7086  fveqressseq  7099  ffvresb  7145  fsnunfv  7207  funfvima  7250  funiunfv  7268  offres  8008  fnwelem  8156  ressuppss  8208  ressuppssdif  8210  frrlem11  8321  frrlem12  8322  smores  8392  smores3  8393  smores2  8394  tz7.44-2  8447  tz7.44-3  8448  frfnom  8475  sbthlem5  9127  sbthlem7  9129  domss2  9176  imafi  9353  ordtypelem4  9561  wdomima2g  9626  r0weon  10052  imadomg  10574  dmaddpi  10930  dmmulpi  10931  ltweuz  14002  dmhashres  14380  limsupgle  15513  fvsetsid  17205  setsdm  17207  setsfun  17208  setsfun0  17209  setsres  17215  lubdm  18396  glbdm  18409  gsumzaddlem  19939  dprdcntz2  20058  lmres  23308  imacmp  23405  qtoptop2  23707  kqdisj  23740  metreslem  24372  setsmstopn  24490  ismbl  25561  mbfres  25679  dvres3a  25949  cpnres  25973  dvlipcn  26033  dvlip2  26034  c1lip3  26038  dvcnvrelem1  26056  dvcvx  26059  dvlog  26693  sltres  27707  nolesgn2ores  27717  nogesgn1ores  27719  nodense  27737  nosupres  27752  nosupbnd1lem1  27753  nosupbnd2lem1  27760  nosupbnd2  27761  noinfres  27767  noinfbnd1lem1  27768  noinfbnd2lem1  27775  noetasuplem2  27779  noetainflem2  27783  uhgrspansubgrlem  29307  trlsegvdeglem4  30242  hlimcaui  31255  ftc2re  34613  dfrdg2  35796  bj-fvsnun2  37257  caures  37767  ssbnd  37795  mapfzcons1  42728  diophrw  42770  eldioph2lem1  42771  eldioph2lem2  42772  tfsconcatrev  43361  limsupresxr  45781  liminfresxr  45782  fourierdlem93  46214  fouriersw  46246  sssmf  46753  eldmressn  47049  fnresfnco  47053  afvres  47184  afv2res  47251  resinsn  48772  resinsnALT  48773  tposrescnv  48779