Theorem dmres 4921

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 2738	. . . . 5 |- x e. _V
2	1	eldm2 4818	. . . 4 |- ( x e. dom ( A |` B ) <-> E. y <. x , y >. e. ( A |` B ) )
3		19.41v 1900	. . . . 5 |- ( E. y ( <. x , y >. e. A /\ x e. B ) <-> ( E. y <. x , y >. e. A /\ x e. B ) )
4		vex 2738	. . . . . . 7 |- y e. _V
5	4	opelres 4905	. . . . . 6 |- ( <. x , y >. e. ( A |` B ) <-> ( <. x , y >. e. A /\ x e. B ) )
6	5	exbii 1603	. . . . 5 |- ( E. y <. x , y >. e. ( A |` B ) <-> E. y ( <. x , y >. e. A /\ x e. B ) )
7	1	eldm2 4818	. . . . . 6 |- ( x e. dom A <-> E. y <. x , y >. e. A )
8	7	anbi1i 458	. . . . 5 |- ( ( x e. dom A /\ x e. B ) <-> ( E. y <. x , y >. e. A /\ x e. B ) )
9	3, 6, 8	3bitr4i 212	. . . 4 |- ( E. y <. x , y >. e. ( A |` B ) <-> ( x e. dom A /\ x e. B ) )
10	2, 9	bitr2i 185	. . 3 |- ( ( x e. dom A /\ x e. B ) <-> x e. dom ( A |` B ) )
11	10	ineqri 3326	. 2 |- ( dom A i^i B ) = dom ( A |` B )
12		incom 3325	. 2 |- ( dom A i^i B ) = ( B i^i dom A )
13	11, 12	eqtr3i 2198	1 |- dom ( A |` B ) = ( B i^i dom A )

Syntax hints:   /\ wa 104   = wceq 1353   E.wex 1490   e. wcel 2146   i^i cin 3126   <.cop 3592   dom cdm 4620   |` cres 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-pow 4169  ax-pr 4203

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458  df-rex 2459  df-v 2737  df-un 3131  df-in 3133  df-ss 3140  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-br 3999  df-opab 4060  df-xp 4626  df-dm 4630  df-res 4632

This theorem is referenced by:  ssdmres  4922  dmresexg  4923  imadisj  4983  ndmima  4998  imainrect  5066  dmresv  5079  resdmres  5112  funimacnv  5284  fnresdisj  5318  fnres  5324  ssimaex  5569  fnreseql  5618  respreima  5636  ffvresb  5671  fsnunfv  5709  funfvima  5739  offres  6126  smores  6283  smores3  6284  smores2  6285  fnfi  6926  sbthlemi5  6950  sbthlem7  6952  dmaddpi  7299  dmmulpi  7300  fvsetsid  12461  setsfun  12462  setsfun0  12463  setsresg  12465  lmres  13317  metreslem  13449