Theorem dmres 6004

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 3476	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5902	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1955	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3476	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5990	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1848	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5902	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi2i 621	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	3, 6, 8	3bitr4i 302	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴))
10	2, 9	bitr2i 275	. . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 4205	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2739	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 394   = wceq 1539  ∃wex 1779   ∈ wcel 2104   ∩ cin 3948  ⟨cop 4635  dom cdm 5677   ↾ cres 5679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-xp 5683  df-dm 5687  df-res 5689

This theorem is referenced by:  ssdmres  6005  dmresexg  6006  dmressnsn  6024  eldmeldmressn  6026  relresdm1  6034  imadisj  6080  imainrect  6181  dmresv  6200  resdmres  6232  resdmss  6235  coeq0  6255  resssxp  6270  snres0  6298  funimacnv  6630  fnresdisj  6671  fnres  6678  fresaunres2  6764  nfvres  6933  ssimaex  6977  fnreseql  7050  respreima  7068  fveqressseq  7082  ffvresb  7127  fsnunfv  7188  funfvima  7235  funiunfv  7251  offres  7974  fnwelem  8121  ressuppss  8172  ressuppssdif  8174  frrlem11  8285  frrlem12  8286  smores  8356  smores3  8357  smores2  8358  tz7.44-2  8411  tz7.44-3  8412  frfnom  8439  sbthlem5  9091  sbthlem7  9093  domss2  9140  imafiALT  9349  ordtypelem4  9520  wdomima2g  9585  r0weon  10011  imadomg  10533  dmaddpi  10889  dmmulpi  10890  ltweuz  13932  dmhashres  14307  limsupgle  15427  fvsetsid  17107  setsdm  17109  setsfun  17110  setsfun0  17111  setsres  17117  lubdm  18310  glbdm  18323  gsumzaddlem  19832  dprdcntz2  19951  lmres  23026  imacmp  23123  qtoptop2  23425  kqdisj  23458  metreslem  24090  setsmstopn  24208  ismbl  25277  mbfres  25395  dvres3a  25665  cpnres  25688  dvlipcn  25745  dvlip2  25746  c1lip3  25750  dvcnvrelem1  25768  dvcvx  25771  dvlog  26393  sltres  27399  nolesgn2ores  27409  nogesgn1ores  27411  nodense  27429  nosupres  27444  nosupbnd1lem1  27445  nosupbnd2lem1  27452  nosupbnd2  27453  noinfres  27459  noinfbnd1lem1  27460  noinfbnd2lem1  27467  noetasuplem2  27471  noetainflem2  27475  uhgrspansubgrlem  28812  trlsegvdeglem4  29741  hlimcaui  30754  ftc2re  33906  dfrdg2  35069  bj-fvsnun2  36442  caures  36933  ssbnd  36961  mapfzcons1  41759  diophrw  41801  eldioph2lem1  41802  eldioph2lem2  41803  tfsconcatrev  42402  dmresss  44233  limsupresxr  44782  liminfresxr  44783  fourierdlem93  45215  fouriersw  45247  sssmf  45754  eldmressn  46047  fnresfnco  46051  afvres  46180  afv2res  46247