Theorem dmres 5972

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

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ∩ cin 3910  ⟨cop 4591  dom cdm 5631   ↾ cres 5633

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-dm 5641  df-res 5643

This theorem is referenced by:  ssdmres  5973  dmresexg  5974  dmressnsn  5983  eldmeldmressn  5985  relresdm1  5993  imadisj  6040  imainrect  6142  dmresv  6161  resdmres  6193  resdmss  6196  coeq0  6216  resssxp  6231  snres0  6259  funimacnv  6581  fnresdisj  6620  fnres  6627  fresaunres2  6714  nfvres  6881  ssimaex  6928  fnreseql  7002  respreima  7020  fveqressseq  7033  ffvresb  7079  fsnunfv  7143  funfvima  7186  funiunfv  7204  offres  7941  fnwelem  8087  ressuppss  8139  ressuppssdif  8141  frrlem11  8252  frrlem12  8253  smores  8298  smores3  8299  smores2  8300  tz7.44-2  8352  tz7.44-3  8353  frfnom  8380  sbthlem5  9032  sbthlem7  9034  domss2  9077  imafi  9240  ordtypelem4  9450  wdomima2g  9515  r0weon  9941  imadomg  10463  dmaddpi  10819  dmmulpi  10820  ltweuz  13902  dmhashres  14282  limsupgle  15419  fvsetsid  17114  setsdm  17116  setsfun  17117  setsfun0  17118  setsres  17124  lubdm  18286  glbdm  18299  gsumzaddlem  19827  dprdcntz2  19946  lmres  23163  imacmp  23260  qtoptop2  23562  kqdisj  23595  metreslem  24226  setsmstopn  24342  ismbl  25403  mbfres  25521  dvres3a  25791  cpnres  25815  dvlipcn  25875  dvlip2  25876  c1lip3  25880  dvcnvrelem1  25898  dvcvx  25901  dvlog  26536  sltres  27550  nolesgn2ores  27560  nogesgn1ores  27562  nodense  27580  nosupres  27595  nosupbnd1lem1  27596  nosupbnd2lem1  27603  nosupbnd2  27604  noinfres  27610  noinfbnd1lem1  27611  noinfbnd2lem1  27618  noetasuplem2  27622  noetainflem2  27626  onsiso  28145  bdayn0sf1o  28235  uhgrspansubgrlem  29193  trlsegvdeglem4  30125  hlimcaui  31138  ftc2re  34562  dfrdg2  35756  bj-fvsnun2  37217  caures  37727  ssbnd  37755  mapfzcons1  42678  diophrw  42720  eldioph2lem1  42721  eldioph2lem2  42722  tfsconcatrev  43310  limsupresxr  45737  liminfresxr  45738  fourierdlem93  46170  fouriersw  46202  sssmf  46709  eldmressn  47011  fnresfnco  47015  afvres  47146  afv2res  47213  resinsn  48833  resinsnALT  48834  tposrescnv  48840