Theorem dmres 5875

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 3497	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5770	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1954	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3497	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5861	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1848	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5770	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi2i 624	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	3, 6, 8	3bitr4i 305	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴))
10	2, 9	bitr2i 278	. . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 4180	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2830	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 398   = wceq 1537  ∃wex 1780   ∈ wcel 2114   ∩ cin 3935  ⟨cop 4573  dom cdm 5555   ↾ cres 5557

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-xp 5561  df-dm 5565  df-res 5567

This theorem is referenced by:  ssdmres  5876  dmresexg  5877  dmressnsn  5894  eldmeldmressn  5896  imadisj  5948  imainrect  6038  dmresv  6057  resdmres  6089  coeq0  6108  funimacnv  6435  fnresdisj  6467  fnres  6474  fresaunres2  6550  nfvres  6706  ssimaex  6748  fnreseql  6818  respreima  6836  fveqressseq  6847  ffvresb  6888  fsnunfv  6949  funfvima  6992  funiunfv  7007  offres  7684  fnwelem  7825  ressuppss  7849  ressuppssdif  7851  smores  7989  smores3  7990  smores2  7991  tz7.44-2  8043  tz7.44-3  8044  frfnom  8070  sbthlem5  8631  sbthlem7  8633  domss2  8676  imafi  8817  ordtypelem4  8985  wdomima2g  9050  r0weon  9438  imadomg  9956  dmaddpi  10312  dmmulpi  10313  ltweuz  13330  dmhashres  13702  limsupgle  14834  fvsetsid  16515  setsdm  16517  setsfun  16518  setsfun0  16519  setsres  16525  lubdm  17589  glbdm  17602  gsumzaddlem  19041  dprdcntz2  19160  lmres  21908  imacmp  22005  qtoptop2  22307  kqdisj  22340  metreslem  22972  setsmstopn  23088  ismbl  24127  mbfres  24245  dvres3a  24512  cpnres  24534  dvlipcn  24591  dvlip2  24592  c1lip3  24596  dvcnvrelem1  24614  dvcvx  24617  dvlog  25234  uhgrspansubgrlem  27072  trlsegvdeglem4  28002  hlimcaui  29013  funresdm1  30355  ftc2re  31869  dfrdg2  33040  frrlem11  33133  frrlem12  33134  sltres  33169  nolesgn2ores  33179  nodense  33196  nosupres  33207  nosupbnd1lem1  33208  nosupbnd2lem1  33215  nosupbnd2  33216  bj-fvsnun2  34541  caures  35050  ssbnd  35081  mapfzcons1  39334  diophrw  39376  eldioph2lem1  39377  eldioph2lem2  39378  rp-imass  40137  dmresss  41521  limsupresxr  42067  liminfresxr  42068  fourierdlem93  42504  fouriersw  42536  sssmf  43035  eldmressn  43292  fnresfnco  43296  afvres  43391  afv2res  43458  setrec2lem1  44816