Theorem dmres 4912

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 2733	. . . . 5 |- x e. _V
2	1	eldm2 4809	. . . 4 |- ( x e. dom ( A |` B ) <-> E. y <. x , y >. e. ( A |` B ) )
3		19.41v 1895	. . . . 5 |- ( E. y ( <. x , y >. e. A /\ x e. B ) <-> ( E. y <. x , y >. e. A /\ x e. B ) )
4		vex 2733	. . . . . . 7 |- y e. _V
5	4	opelres 4896	. . . . . 6 |- ( <. x , y >. e. ( A |` B ) <-> ( <. x , y >. e. A /\ x e. B ) )
6	5	exbii 1598	. . . . 5 |- ( E. y <. x , y >. e. ( A |` B ) <-> E. y ( <. x , y >. e. A /\ x e. B ) )
7	1	eldm2 4809	. . . . . 6 |- ( x e. dom A <-> E. y <. x , y >. e. A )
8	7	anbi1i 455	. . . . 5 |- ( ( x e. dom A /\ x e. B ) <-> ( E. y <. x , y >. e. A /\ x e. B ) )
9	3, 6, 8	3bitr4i 211	. . . 4 |- ( E. y <. x , y >. e. ( A |` B ) <-> ( x e. dom A /\ x e. B ) )
10	2, 9	bitr2i 184	. . 3 |- ( ( x e. dom A /\ x e. B ) <-> x e. dom ( A |` B ) )
11	10	ineqri 3320	. 2 |- ( dom A i^i B ) = dom ( A |` B )
12		incom 3319	. 2 |- ( dom A i^i B ) = ( B i^i dom A )
13	11, 12	eqtr3i 2193	1 |- dom ( A |` B ) = ( B i^i dom A )

Syntax hints:   /\ wa 103   = wceq 1348   E.wex 1485   e. wcel 2141   i^i cin 3120   <.cop 3586   dom cdm 4611   |` cres 4613

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-pow 4160  ax-pr 4194

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-br 3990  df-opab 4051  df-xp 4617  df-dm 4621  df-res 4623

This theorem is referenced by:  ssdmres  4913  dmresexg  4914  imadisj  4973  ndmima  4988  imainrect  5056  dmresv  5069  resdmres  5102  funimacnv  5274  fnresdisj  5308  fnres  5314  ssimaex  5557  fnreseql  5606  respreima  5624  ffvresb  5659  fsnunfv  5697  funfvima  5727  offres  6114  smores  6271  smores3  6272  smores2  6273  fnfi  6914  sbthlemi5  6938  sbthlem7  6940  dmaddpi  7287  dmmulpi  7288  fvsetsid  12450  setsfun  12451  setsfun0  12452  setsresg  12454  lmres  13042  metreslem  13174