Theorem dmres 5964

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 3435	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5843	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1960	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3435	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5939	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1855	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5843	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi2i 629	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	3, 6, 8	3bitr4i 304	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴))
10	2, 9	bitr2i 277	. . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 4141	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2748	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119   ∩ cin 3882  ⟨cop 4561  dom cdm 5618   ↾ cres 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624  df-dm 5628  df-res 5630

This theorem is referenced by:  ssdmres  5965  dmresexg  5966  dmressnsn  5975  eldmeldmressn  5977  relresdm1  5985  imadisj  6032  imainrect  6132  dmresv  6151  resdmres  6183  resdmss  6186  coeq0  6207  resssxp  6221  snres0  6249  funimacnv  6566  fnresdisj  6605  fnres  6612  fresaunres2  6699  nfvres  6865  ssimaex  6912  fnreseql  6989  respreima  7007  fveqressseq  7020  ffvresb  7067  fsnunfv  7131  funfvima  7174  funiunfv  7192  offres  7925  fnwelem  8071  ressuppss  8123  ressuppssdif  8125  frrlem11  8236  frrlem12  8237  smores  8282  smores3  8283  smores2  8284  tz7.44-2  8336  tz7.44-3  8337  frfnom  8364  sbthlem5  9019  sbthlem7  9021  domss2  9064  imafi  9215  ordtypelem4  9426  wdomima2g  9491  r0weon  9925  imadomg  10447  dmaddpi  10804  dmmulpi  10805  ltweuz  13914  dmhashres  14294  limsupgle  15430  fvsetsid  17129  setsdm  17131  setsfun  17132  setsfun0  17133  setsres  17139  lubdm  18306  glbdm  18319  gsumzaddlem  19887  dprdcntz2  20006  lmres  23283  imacmp  23380  qtoptop2  23682  kqdisj  23715  metreslem  24345  setsmstopn  24461  ismbl  25511  mbfres  25629  dvres3a  25899  cpnres  25922  dvlipcn  25979  dvlip2  25980  c1lip3  25984  dvcnvrelem1  26002  dvcvx  26005  dvlog  26633  ltsres  27644  nolesgn2ores  27654  nogesgn1ores  27656  nodense  27674  nosupres  27689  nosupbnd1lem1  27690  nosupbnd2lem1  27697  nosupbnd2  27698  noinfres  27704  noinfbnd1lem1  27705  noinfbnd2lem1  27712  noetasuplem2  27716  noetainflem2  27720  oniso  28281  bdayn0sf1o  28380  uhgrspansubgrlem  29377  trlsegvdeglem4  30311  hlimcaui  31325  ftc2re  34782  dfrdg2  36021  bj-fvsnun2  37616  caures  38127  ssbnd  38155  dmcnvepres  38757  dmuncnvepres  38758  dmxrncnvepres2  38800  mapfzcons1  43166  diophrw  43208  eldioph2lem1  43209  eldioph2lem2  43210  tfsconcatrev  43793  limsupresxr  46209  liminfresxr  46210  fourierdlem93  46642  fouriersw  46674  sssmf  47181  eldmressn  47500  fnresfnco  47504  afvres  47635  afv2res  47702  resinsn  49362  resinsnALT  49363  tposrescnv  49369