Theorem dmres 5977

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 3433	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5856	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1955	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3433	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5952	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1850	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5856	. . . . . 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 4152	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2745	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ∩ cin 3888  ⟨cop 4573  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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-dm 5641  df-res 5643

This theorem is referenced by:  ssdmres  5978  dmresexg  5979  dmressnsn  5988  eldmeldmressn  5990  relresdm1  5998  imadisj  6045  imainrect  6145  dmresv  6164  resdmres  6196  resdmss  6199  coeq0  6220  resssxp  6234  snres0  6262  funimacnv  6579  fnresdisj  6618  fnres  6625  fresaunres2  6712  nfvres  6878  ssimaex  6925  fnreseql  7000  respreima  7018  fveqressseq  7031  ffvresb  7078  fsnunfv  7142  funfvima  7185  funiunfv  7203  offres  7936  fnwelem  8081  ressuppss  8133  ressuppssdif  8135  frrlem11  8246  frrlem12  8247  smores  8292  smores3  8293  smores2  8294  tz7.44-2  8346  tz7.44-3  8347  frfnom  8374  sbthlem5  9029  sbthlem7  9031  domss2  9074  imafi  9225  ordtypelem4  9436  wdomima2g  9501  r0weon  9934  imadomg  10456  dmaddpi  10813  dmmulpi  10814  ltweuz  13923  dmhashres  14303  limsupgle  15439  fvsetsid  17138  setsdm  17140  setsfun  17141  setsfun0  17142  setsres  17148  lubdm  18315  glbdm  18328  gsumzaddlem  19896  dprdcntz2  20015  lmres  23265  imacmp  23362  qtoptop2  23664  kqdisj  23697  metreslem  24327  setsmstopn  24443  ismbl  25493  mbfres  25611  dvres3a  25881  cpnres  25904  dvlipcn  25961  dvlip2  25962  c1lip3  25966  dvcnvrelem1  25984  dvcvx  25987  dvlog  26615  ltsres  27626  nolesgn2ores  27636  nogesgn1ores  27638  nodense  27656  nosupres  27671  nosupbnd1lem1  27672  nosupbnd2lem1  27679  nosupbnd2  27680  noinfres  27686  noinfbnd1lem1  27687  noinfbnd2lem1  27694  noetasuplem2  27698  noetainflem2  27702  oniso  28263  bdayn0sf1o  28362  uhgrspansubgrlem  29359  trlsegvdeglem4  30293  hlimcaui  31307  ftc2re  34742  dfrdg2  35975  bj-fvsnun2  37570  caures  38081  ssbnd  38109  dmcnvepres  38711  dmuncnvepres  38712  dmxrncnvepres2  38754  mapfzcons1  43149  diophrw  43191  eldioph2lem1  43192  eldioph2lem2  43193  tfsconcatrev  43776  limsupresxr  46194  liminfresxr  46195  fourierdlem93  46627  fouriersw  46659  sssmf  47166  eldmressn  47485  fnresfnco  47489  afvres  47620  afv2res  47687  resinsn  49347  resinsnALT  49348  tposrescnv  49354