Theorem dmres 5143

Description: The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
dmres	|- dom ( A |` B ) = ( B i^i dom A )

Proof of Theorem dmres

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2987	. . . . 5 |- x e. _V
2	1	eldm2 5050	. . . 4 |- ( x e. dom ( A |` B ) <-> E. y <. x , y >. e. ( A |` B ) )
3		19.41v 1920	. . . . 5 |- ( E. y ( <. x , y >. e. A /\ x e. B ) <-> ( E. y <. x , y >. e. A /\ x e. B ) )
4		vex 2987	. . . . . . 7 |- y e. _V
5	4	opelres 5128	. . . . . 6 |- ( <. x , y >. e. ( A |` B ) <-> ( <. x , y >. e. A /\ x e. B ) )
6	5	exbii 1634	. . . . 5 |- ( E. y <. x , y >. e. ( A |` B ) <-> E. y ( <. x , y >. e. A /\ x e. B ) )
7	1	eldm2 5050	. . . . . 6 |- ( x e. dom A <-> E. y <. x , y >. e. A )
8	7	anbi1i 695	. . . . 5 |- ( ( x e. dom A /\ x e. B ) <-> ( E. y <. x , y >. e. A /\ x e. B ) )
9	3, 6, 8	3bitr4i 277	. . . 4 |- ( E. y <. x , y >. e. ( A |` B ) <-> ( x e. dom A /\ x e. B ) )
10	2, 9	bitr2i 250	. . 3 |- ( ( x e. dom A /\ x e. B ) <-> x e. dom ( A |` B ) )
11	10	ineqri 3556	. 2 |- ( dom A i^i B ) = dom ( A |` B )
12		incom 3555	. 2 |- ( dom A i^i B ) = ( B i^i dom A )
13	11, 12	eqtr3i 2465	1 |- dom ( A |` B ) = ( B i^i dom A )

Syntax hints:   /\ wa 369   = wceq 1369   E.wex 1586   e. wcel 1756   i^i cin 3339   <.cop 3895   dom cdm 4852   |` cres 4854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pr 4543

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896  df-br 4305  df-opab 4363  df-xp 4858  df-dm 4862  df-res 4864

This theorem is referenced by:  ssdmres  5144  dmresexg  5145  imadisj  5200  ndmima  5217  imainrect  5291  dmresv  5308  resdmres  5341  funimacnv  5502  fnresdisj  5533  fnres  5539  fresaunres2  5595  nfvres  5732  ssimaex  5768  fnreseql  5825  respreima  5844  ffvresb  5886  fsnunfv  5930  funfvima  5964  funiunfv  5977  offres  6584  fnwelem  6699  ressuppss  6720  ressuppssdif  6722  smores  6825  smores3  6826  smores2  6827  tz7.44-2  6875  tz7.44-3  6876  frfnom  6902  sbthlem5  7437  sbthlem7  7439  domss2  7482  imafi  7616  ordtypelem4  7747  wdomima2g  7813  r0weon  8191  imadomg  8713  dmaddpi  9071  dmmulpi  9072  ltweuz  11796  dmhashres  12124  limsupgle  12967  fvsetsid  14211  setsres  14214  lubdm  15161  glbdm  15174  gsumzaddlem  16420  gsumzaddlemOLD  16422  dprdcntz2  16548  lmres  18916  imacmp  19012  qtoptop2  19284  kqdisj  19317  metreslem  19949  setsmstopn  20065  ismbl  21021  mbfres  21134  dvres3a  21401  cpnres  21423  dvlipcn  21478  dvlip2  21479  c1lip3  21483  dvcnvrelem1  21501  dvcvx  21504  dvlog  22108  cusgrasizeindslem2  23394  eupares  23608  hlimcaui  24651  gsumle  26258  dfrdg2  27621  sltres  27817  nodense  27842  nofulllem5  27859  caures  28668  ssbnd  28699  mapfzcons1  29065  coeq0  29102  diophrw  29109  eldioph2lem1  29110  eldioph2lem2  29111  eldmressn  30039  dmressnsn  30040  fnresfnco  30044  afvres  30090  eldmeldmressn  30152