Theorem dmres 5968

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 3441	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5847	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1954	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3441	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5943	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1849	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5847	. . . . . 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 4161	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2742	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113   ∩ cin 3897  ⟨cop 4583  dom cdm 5621   ↾ cres 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-xp 5627  df-dm 5631  df-res 5633

This theorem is referenced by:  ssdmres  5969  dmresexg  5970  dmressnsn  5979  eldmeldmressn  5981  relresdm1  5989  imadisj  6036  imainrect  6136  dmresv  6155  resdmres  6187  resdmss  6190  coeq0  6211  resssxp  6225  snres0  6253  funimacnv  6570  fnresdisj  6609  fnres  6616  fresaunres2  6703  nfvres  6869  ssimaex  6916  fnreseql  6990  respreima  7008  fveqressseq  7021  ffvresb  7067  fsnunfv  7130  funfvima  7173  funiunfv  7191  offres  7924  fnwelem  8070  ressuppss  8122  ressuppssdif  8124  frrlem11  8235  frrlem12  8236  smores  8281  smores3  8282  smores2  8283  tz7.44-2  8335  tz7.44-3  8336  frfnom  8363  sbthlem5  9015  sbthlem7  9017  domss2  9060  imafi  9210  ordtypelem4  9418  wdomima2g  9483  r0weon  9914  imadomg  10436  dmaddpi  10792  dmmulpi  10793  ltweuz  13875  dmhashres  14255  limsupgle  15391  fvsetsid  17086  setsdm  17088  setsfun  17089  setsfun0  17090  setsres  17096  lubdm  18263  glbdm  18276  gsumzaddlem  19841  dprdcntz2  19960  lmres  23235  imacmp  23332  qtoptop2  23634  kqdisj  23667  metreslem  24297  setsmstopn  24413  ismbl  25474  mbfres  25592  dvres3a  25862  cpnres  25886  dvlipcn  25946  dvlip2  25947  c1lip3  25951  dvcnvrelem1  25969  dvcvx  25972  dvlog  26607  sltres  27621  nolesgn2ores  27631  nogesgn1ores  27633  nodense  27651  nosupres  27666  nosupbnd1lem1  27667  nosupbnd2lem1  27674  nosupbnd2  27675  noinfres  27681  noinfbnd1lem1  27682  noinfbnd2lem1  27689  noetasuplem2  27693  noetainflem2  27697  onsiso  28225  bdayn0sf1o  28315  uhgrspansubgrlem  29289  trlsegvdeglem4  30224  hlimcaui  31237  ftc2re  34683  dfrdg2  35909  bj-fvsnun2  37373  caures  37873  ssbnd  37901  dmcnvepres  38487  dmuncnvepres  38488  dmxrncnvepres2  38530  mapfzcons1  42874  diophrw  42916  eldioph2lem1  42917  eldioph2lem2  42918  tfsconcatrev  43505  limsupresxr  45926  liminfresxr  45927  fourierdlem93  46359  fouriersw  46391  sssmf  46898  eldmressn  47199  fnresfnco  47203  afvres  47334  afv2res  47401  resinsn  49033  resinsnALT  49034  tposrescnv  49040