Theorem dmres 5293

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 3116	. . . . 5 |- x e. _V
2	1	eldm2 5200	. . . 4 |- ( x e. dom ( A |` B ) <-> E. y <. x , y >. e. ( A |` B ) )
3		19.41v 1945	. . . . 5 |- ( E. y ( <. x , y >. e. A /\ x e. B ) <-> ( E. y <. x , y >. e. A /\ x e. B ) )
4		vex 3116	. . . . . . 7 |- y e. _V
5	4	opelres 5278	. . . . . 6 |- ( <. x , y >. e. ( A |` B ) <-> ( <. x , y >. e. A /\ x e. B ) )
6	5	exbii 1644	. . . . 5 |- ( E. y <. x , y >. e. ( A |` B ) <-> E. y ( <. x , y >. e. A /\ x e. B ) )
7	1	eldm2 5200	. . . . . 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 3692	. 2 |- ( dom A i^i B ) = dom ( A |` B )
12		incom 3691	. 2 |- ( dom A i^i B ) = ( B i^i dom A )
13	11, 12	eqtr3i 2498	1 |- dom ( A |` B ) = ( B i^i dom A )

Syntax hints:   /\ wa 369   = wceq 1379   E.wex 1596   e. wcel 1767   i^i cin 3475   <.cop 4033   dom cdm 4999   |` cres 5001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-xp 5005  df-dm 5009  df-res 5011

This theorem is referenced by:  ssdmres  5294  dmresexg  5295  dmressnsn  5311  eldmeldmressn  5313  imadisj  5355  ndmima  5372  imainrect  5447  dmresv  5464  resdmres  5497  coeq0  5515  funimacnv  5659  fnresdisj  5690  fnres  5696  fresaunres2  5756  nfvres  5895  ssimaex  5931  fnreseql  5990  respreima  6009  ffvresb  6051  fsnunfv  6100  funfvima  6134  funiunfv  6147  offres  6779  fnwelem  6898  ressuppss  6919  ressuppssdif  6921  smores  7023  smores3  7024  smores2  7025  tz7.44-2  7073  tz7.44-3  7074  frfnom  7100  sbthlem5  7631  sbthlem7  7633  domss2  7676  imafi  7812  ordtypelem4  7945  wdomima2g  8011  r0weon  8389  imadomg  8911  dmaddpi  9267  dmmulpi  9268  ltweuz  12039  dmhashres  12381  limsupgle  13262  fvsetsid  14514  setsres  14517  lubdm  15465  glbdm  15478  gsumzaddlem  16734  gsumzaddlemOLD  16736  dprdcntz2  16885  lmres  19583  imacmp  19679  qtoptop2  19951  kqdisj  19984  metreslem  20616  setsmstopn  20732  ismbl  21688  mbfres  21802  dvres3a  22069  cpnres  22091  dvlipcn  22146  dvlip2  22147  c1lip3  22151  dvcnvrelem1  22169  dvcvx  22172  dvlog  22776  cusgrasizeindslem2  24166  eupares  24667  hlimcaui  25846  dfrdg2  28821  sltres  29017  nodense  29042  nofulllem5  29059  caures  29872  ssbnd  29903  mapfzcons1  30269  diophrw  30312  eldioph2lem1  30313  eldioph2lem2  30314  fourierdlem93  31516  fouriersw  31548  eldmressn  31691  fnresfnco  31694  afvres  31740  rp-imass  36805