Theorem dmres 5304

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 3112	. . . . 5 |- x e. _V
2	1	eldm2 5211	. . . 4 |- ( x e. dom ( A |` B ) <-> E. y <. x , y >. e. ( A |` B ) )
3		19.41v 1772	. . . . 5 |- ( E. y ( <. x , y >. e. A /\ x e. B ) <-> ( E. y <. x , y >. e. A /\ x e. B ) )
4		vex 3112	. . . . . . 7 |- y e. _V
5	4	opelres 5289	. . . . . 6 |- ( <. x , y >. e. ( A |` B ) <-> ( <. x , y >. e. A /\ x e. B ) )
6	5	exbii 1668	. . . . 5 |- ( E. y <. x , y >. e. ( A |` B ) <-> E. y ( <. x , y >. e. A /\ x e. B ) )
7	1	eldm2 5211	. . . . . 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 3688	. 2 |- ( dom A i^i B ) = dom ( A |` B )
12		incom 3687	. 2 |- ( dom A i^i B ) = ( B i^i dom A )
13	11, 12	eqtr3i 2488	1 |- dom ( A |` B ) = ( B i^i dom A )

Syntax hints:   /\ wa 369   = wceq 1395   E.wex 1613   e. wcel 1819   i^i cin 3470   <.cop 4038   dom cdm 5008   |` cres 5010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pr 4695

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-br 4457  df-opab 4516  df-xp 5014  df-dm 5018  df-res 5020

This theorem is referenced by:  ssdmres  5305  dmresexg  5306  dmressnsn  5322  eldmeldmressn  5324  imadisj  5366  ndmima  5383  imainrect  5455  dmresv  5471  resdmres  5504  coeq0  5522  funimacnv  5666  fnresdisj  5697  fnres  5703  fresaunres2  5763  nfvres  5902  ssimaex  5938  fnreseql  5998  respreima  6017  fveqressseq  6028  ffvresb  6063  fsnunfv  6112  funfvima  6148  funiunfv  6161  offres  6794  fnwelem  6914  ressuppss  6937  ressuppssdif  6939  smores  7041  smores3  7042  smores2  7043  tz7.44-2  7091  tz7.44-3  7092  frfnom  7118  sbthlem5  7650  sbthlem7  7652  domss2  7695  imafi  7831  ordtypelem4  7964  wdomima2g  8030  r0weon  8407  imadomg  8929  dmaddpi  9285  dmmulpi  9286  ltweuz  12075  dmhashres  12417  limsupgle  13312  fvsetsid  14671  setsres  14674  lubdm  15736  glbdm  15749  gsumzaddlem  17061  gsumzaddlemOLD  17063  dprdcntz2  17213  lmres  19928  imacmp  20024  qtoptop2  20326  kqdisj  20359  metreslem  20991  setsmstopn  21107  ismbl  22063  mbfres  22177  dvres3a  22444  cpnres  22466  dvlipcn  22521  dvlip2  22522  c1lip3  22526  dvcnvrelem1  22544  dvcvx  22547  dvlog  23158  cusgrasizeindslem2  24601  eupares  25102  hlimcaui  26281  dfrdg2  29445  sltres  29641  nodense  29666  nofulllem5  29683  caures  30458  ssbnd  30489  mapfzcons1  30854  diophrw  30897  eldioph2lem1  30898  eldioph2lem2  30899  fourierdlem93  32185  fouriersw  32217  eldmressn  32411  fnresfnco  32414  afvres  32460  rp-imass  37985