Theorem dmres 5419

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 3203	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5322	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.41v 1914	. . . . 5 ⊢ (∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
4		vex 3203	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelres 5401	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
6	5	exbii 1774	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
7	1	eldm2 5322	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi1i 731	. . . . 5 ⊢ ((𝑥 ∈ dom 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
9	3, 6, 8	3bitr4i 292	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ dom 𝐴 ∧ 𝑥 ∈ 𝐵))
10	2, 9	bitr2i 265	. . 3 ⊢ ((𝑥 ∈ dom 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 3806	. 2 ⊢ (dom 𝐴 ∩ 𝐵) = dom (𝐴 ↾ 𝐵)
12		incom 3805	. 2 ⊢ (dom 𝐴 ∩ 𝐵) = (𝐵 ∩ dom 𝐴)
13	11, 12	eqtr3i 2646	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 384   = wceq 1483  ∃wex 1704   ∈ wcel 1990   ∩ cin 3573  ⟨cop 4183  dom cdm 5114   ↾ cres 5116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-xp 5120  df-dm 5124  df-res 5126

This theorem is referenced by:  ssdmres  5420  dmresexg  5421  dmressnsn  5438  eldmeldmressn  5440  imadisj  5484  imainrect  5575  dmresv  5593  resdmres  5625  coeq0  5644  funimacnv  5970  fnresdisj  6001  fnres  6007  fresaunres2  6076  nfvres  6224  ssimaex  6263  fnreseql  6327  respreima  6344  fveqressseq  6355  ffvresb  6394  fsnunfv  6453  funfvima  6492  funiunfv  6506  offres  7163  fnwelem  7292  ressuppss  7314  ressuppssdif  7316  smores  7449  smores3  7450  smores2  7451  tz7.44-2  7503  tz7.44-3  7504  frfnom  7530  sbthlem5  8074  sbthlem7  8076  domss2  8119  imafi  8259  ordtypelem4  8426  wdomima2g  8491  r0weon  8835  imadomg  9356  dmaddpi  9712  dmmulpi  9713  ltweuz  12760  dmhashres  13129  limsupgle  14208  fvsetsid  15890  setsdm  15892  setsfun  15893  setsfun0  15894  setsres  15901  lubdm  16979  glbdm  16992  gsumzaddlem  18321  dprdcntz2  18437  lmres  21104  imacmp  21200  qtoptop2  21502  kqdisj  21535  metreslem  22167  setsmstopn  22283  ismbl  23294  mbfres  23411  dvres3a  23678  cpnres  23700  dvlipcn  23757  dvlip2  23758  c1lip3  23762  dvcnvrelem1  23780  dvcvx  23783  dvlog  24397  uhgrspansubgrlem  26182  wlkres  26567  trlsegvdeglem4  27083  hlimcaui  28093  funresdm1  29416  ftc2re  30676  dfrdg2  31701  sltres  31815  nolesgn2ores  31825  nodense  31842  nosupres  31853  nosupbnd1lem1  31854  nosupbnd2lem1  31861  nosupbnd2  31862  caures  33556  ssbnd  33587  mapfzcons1  37280  diophrw  37322  eldioph2lem1  37323  eldioph2lem2  37324  rp-imass  38065  dmresss  39436  limsupresxr  39998  liminfresxr  39999  fourierdlem93  40416  fouriersw  40448  sssmf  40947  eldmressn  41203  fnresfnco  41206  afvres  41252  setrec2lem1  42440