Theorem dmres 5040

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 2806	. . . . 5 |- x e. _V
2	1	eldm2 4935	. . . 4 |- ( x e. dom ( A |` B ) <-> E. y <. x , y >. e. ( A |` B ) )
3		19.41v 1951	. . . . 5 |- ( E. y ( <. x , y >. e. A /\ x e. B ) <-> ( E. y <. x , y >. e. A /\ x e. B ) )
4		vex 2806	. . . . . . 7 |- y e. _V
5	4	opelres 5024	. . . . . 6 |- ( <. x , y >. e. ( A |` B ) <-> ( <. x , y >. e. A /\ x e. B ) )
6	5	exbii 1654	. . . . 5 |- ( E. y <. x , y >. e. ( A |` B ) <-> E. y ( <. x , y >. e. A /\ x e. B ) )
7	1	eldm2 4935	. . . . . 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 3402	. 2 |- ( dom A i^i B ) = dom ( A |` B )
12		incom 3401	. 2 |- ( dom A i^i B ) = ( B i^i dom A )
13	11, 12	eqtr3i 2254	1 |- dom ( A |` B ) = ( B i^i dom A )

Syntax hints:   /\ wa 104   = wceq 1398   E.wex 1541   e. wcel 2202   i^i cin 3200   <.cop 3676   dom cdm 4731   |` cres 4733

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094  df-opab 4156  df-xp 4737  df-dm 4741  df-res 4743

This theorem is referenced by:  ssdmres  5041  dmresexg  5042  imadisj  5105  ndmima  5120  imainrect  5189  dmresv  5202  resdmres  5235  funimacnv  5413  fnresdisj  5449  fnres  5456  ssimaex  5716  fnreseql  5766  respreima  5783  ffvresb  5818  fsnunfv  5863  funfvima  5896  offres  6306  ressuppss  6432  smores  6501  smores3  6502  smores2  6503  fnfi  7178  sbthlemi5  7203  sbthlem7  7205  dmaddpi  7605  dmmulpi  7606  fvsetsid  13196  setsfun  13197  setsfun0  13198  setsresg  13200  bassetsnn  13219  lmres  15059  metreslem  15191  uhgrspansubgrlem  16217  trlsegvdeglem4  16404