Theorem dmres 5979

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

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ∩ cin 3902  ⟨cop 4588  dom cdm 5632   ↾ cres 5634

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 2709  ax-sep 5243  ax-pr 5379

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 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-dm 5642  df-res 5644

This theorem is referenced by:  ssdmres  5980  dmresexg  5981  dmressnsn  5990  eldmeldmressn  5992  relresdm1  6000  imadisj  6047  imainrect  6147  dmresv  6166  resdmres  6198  resdmss  6201  coeq0  6222  resssxp  6236  snres0  6264  funimacnv  6581  fnresdisj  6620  fnres  6627  fresaunres2  6714  nfvres  6880  ssimaex  6927  fnreseql  7002  respreima  7020  fveqressseq  7033  ffvresb  7080  fsnunfv  7143  funfvima  7186  funiunfv  7204  offres  7937  fnwelem  8083  ressuppss  8135  ressuppssdif  8137  frrlem11  8248  frrlem12  8249  smores  8294  smores3  8295  smores2  8296  tz7.44-2  8348  tz7.44-3  8349  frfnom  8376  sbthlem5  9031  sbthlem7  9033  domss2  9076  imafi  9227  ordtypelem4  9438  wdomima2g  9503  r0weon  9934  imadomg  10456  dmaddpi  10813  dmmulpi  10814  ltweuz  13896  dmhashres  14276  limsupgle  15412  fvsetsid  17107  setsdm  17109  setsfun  17110  setsfun0  17111  setsres  17117  lubdm  18284  glbdm  18297  gsumzaddlem  19862  dprdcntz2  19981  lmres  23256  imacmp  23353  qtoptop2  23655  kqdisj  23688  metreslem  24318  setsmstopn  24434  ismbl  25495  mbfres  25613  dvres3a  25883  cpnres  25907  dvlipcn  25967  dvlip2  25968  c1lip3  25972  dvcnvrelem1  25990  dvcvx  25993  dvlog  26628  ltsres  27642  nolesgn2ores  27652  nogesgn1ores  27654  nodense  27672  nosupres  27687  nosupbnd1lem1  27688  nosupbnd2lem1  27695  nosupbnd2  27696  noinfres  27702  noinfbnd1lem1  27703  noinfbnd2lem1  27710  noetasuplem2  27714  noetainflem2  27718  oniso  28279  bdayn0sf1o  28378  uhgrspansubgrlem  29375  trlsegvdeglem4  30310  hlimcaui  31324  ftc2re  34776  dfrdg2  36009  bj-fvsnun2  37511  caures  38011  ssbnd  38039  dmcnvepres  38641  dmuncnvepres  38642  dmxrncnvepres2  38684  mapfzcons1  43074  diophrw  43116  eldioph2lem1  43117  eldioph2lem2  43118  tfsconcatrev  43705  limsupresxr  46124  liminfresxr  46125  fourierdlem93  46557  fouriersw  46589  sssmf  47096  eldmressn  47397  fnresfnco  47401  afvres  47532  afv2res  47599  resinsn  49231  resinsnALT  49232  tposrescnv  49238