Theorem dmres 5113

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 3061	. . . . 5 |- x e. _V
2	1	eldm2 5021	. . . 4 |- ( x e. dom ( A |` B ) <-> E. y <. x , y >. e. ( A |` B ) )
3		19.41v 1795	. . . . 5 |- ( E. y ( <. x , y >. e. A /\ x e. B ) <-> ( E. y <. x , y >. e. A /\ x e. B ) )
4		vex 3061	. . . . . . 7 |- y e. _V
5	4	opelres 5098	. . . . . 6 |- ( <. x , y >. e. ( A |` B ) <-> ( <. x , y >. e. A /\ x e. B ) )
6	5	exbii 1688	. . . . 5 |- ( E. y <. x , y >. e. ( A |` B ) <-> E. y ( <. x , y >. e. A /\ x e. B ) )
7	1	eldm2 5021	. . . . . 6 |- ( x e. dom A <-> E. y <. x , y >. e. A )
8	7	anbi1i 693	. . . . 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 3632	. 2 |- ( dom A i^i B ) = dom ( A |` B )
12		incom 3631	. 2 |- ( dom A i^i B ) = ( B i^i dom A )
13	11, 12	eqtr3i 2433	1 |- dom ( A |` B ) = ( B i^i dom A )

Syntax hints:   /\ wa 367   = wceq 1405   E.wex 1633   e. wcel 1842   i^i cin 3412   <.cop 3977   dom cdm 4822   |` cres 4824

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-br 4395  df-opab 4453  df-xp 4828  df-dm 4832  df-res 4834

This theorem is referenced by:  ssdmres  5114  dmresexg  5115  dmressnsn  5131  eldmeldmressn  5133  imadisj  5175  ndmimaOLD  5193  imainrect  5265  dmresv  5281  resdmres  5313  coeq0  5331  funimacnv  5640  fnresdisj  5671  fnres  5677  fresaunres2  5739  nfvres  5878  ssimaex  5913  fnreseql  5974  respreima  5993  fveqressseq  6004  ffvresb  6040  fsnunfv  6090  funfvima  6127  funiunfv  6140  offres  6778  fnwelem  6898  ressuppss  6921  ressuppssdif  6923  smores  7055  smores3  7056  smores2  7057  tz7.44-2  7109  tz7.44-3  7110  frfnom  7136  sbthlem5  7668  sbthlem7  7670  domss2  7713  imafi  7846  ordtypelem4  7979  wdomima2g  8045  r0weon  8421  imadomg  8943  dmaddpi  9297  dmmulpi  9298  ltweuz  12111  dmhashres  12459  limsupgle  13447  fvsetsid  14866  setsres  14869  lubdm  15931  glbdm  15944  gsumzaddlem  17256  gsumzaddlemOLD  17258  dprdcntz2  17404  lmres  20092  imacmp  20188  qtoptop2  20490  kqdisj  20523  metreslem  21155  setsmstopn  21271  ismbl  22227  mbfres  22341  dvres3a  22608  cpnres  22630  dvlipcn  22685  dvlip2  22686  c1lip3  22690  dvcnvrelem1  22708  dvcvx  22711  dvlog  23324  cusgrasizeindslem2  24878  eupares  25379  hlimcaui  26554  dfrdg2  30002  sltres  30111  nodense  30136  nofulllem5  30153  caures  31515  ssbnd  31546  mapfzcons1  34991  diophrw  35033  eldioph2lem1  35034  eldioph2lem2  35035  rp-imass  35731  fourierdlem93  37331  fouriersw  37363  eldmressn  37557  fnresfnco  37560  afvres  37606