Theorem dmres 5142

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 3085	. . . . 5 |- x e. _V
2	1	eldm2 5050	. . . 4 |- ( x e. dom ( A |` B ) <-> E. y <. x , y >. e. ( A |` B ) )
3		19.41v 1820	. . . . 5 |- ( E. y ( <. x , y >. e. A /\ x e. B ) <-> ( E. y <. x , y >. e. A /\ x e. B ) )
4		vex 3085	. . . . . . 7 |- y e. _V
5	4	opelres 5127	. . . . . 6 |- ( <. x , y >. e. ( A |` B ) <-> ( <. x , y >. e. A /\ x e. B ) )
6	5	exbii 1713	. . . . 5 |- ( E. y <. x , y >. e. ( A |` B ) <-> E. y ( <. x , y >. e. A /\ x e. B ) )
7	1	eldm2 5050	. . . . . 6 |- ( x e. dom A <-> E. y <. x , y >. e. A )
8	7	anbi1i 700	. . . . 5 |- ( ( x e. dom A /\ x e. B ) <-> ( E. y <. x , y >. e. A /\ x e. B ) )
9	3, 6, 8	3bitr4i 281	. . . 4 |- ( E. y <. x , y >. e. ( A |` B ) <-> ( x e. dom A /\ x e. B ) )
10	2, 9	bitr2i 254	. . 3 |- ( ( x e. dom A /\ x e. B ) <-> x e. dom ( A |` B ) )
11	10	ineqri 3657	. 2 |- ( dom A i^i B ) = dom ( A |` B )
12		incom 3656	. 2 |- ( dom A i^i B ) = ( B i^i dom A )
13	11, 12	eqtr3i 2454	1 |- dom ( A |` B ) = ( B i^i dom A )

Syntax hints:   /\ wa 371   = wceq 1438   E.wex 1660   e. wcel 1869   i^i cin 3436   <.cop 4003   dom cdm 4851   |` cres 4853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-br 4422  df-opab 4481  df-xp 4857  df-dm 4861  df-res 4863

This theorem is referenced by:  ssdmres  5143  dmresexg  5144  dmressnsn  5160  eldmeldmressn  5162  imadisj  5204  ndmimaOLD  5223  imainrect  5295  dmresv  5311  resdmres  5343  coeq0  5361  funimacnv  5671  fnresdisj  5702  fnres  5708  fresaunres2  5770  nfvres  5909  ssimaex  5944  fnreseql  6005  respreima  6022  fveqressseq  6031  ffvresb  6067  fsnunfv  6117  funfvima  6153  funiunfv  6166  offres  6800  fnwelem  6920  ressuppss  6943  ressuppssdif  6945  smores  7077  smores3  7078  smores2  7079  tz7.44-2  7131  tz7.44-3  7132  frfnom  7158  sbthlem5  7690  sbthlem7  7692  domss2  7735  imafi  7871  ordtypelem4  8040  wdomima2g  8105  r0weon  8446  imadomg  8964  dmaddpi  9317  dmmulpi  9318  ltweuz  12176  dmhashres  12525  limsupgle  13528  fvsetsid  15141  setsres  15144  lubdm  16218  glbdm  16231  gsumzaddlem  17547  dprdcntz2  17664  lmres  20308  imacmp  20404  qtoptop2  20706  kqdisj  20739  metreslem  21369  setsmstopn  21485  ismbl  22472  mbfres  22592  dvres3a  22861  cpnres  22883  dvlipcn  22938  dvlip2  22939  c1lip3  22943  dvcnvrelem1  22961  dvcvx  22964  dvlog  23588  cusgrasizeindslem2  25194  eupares  25695  hlimcaui  26881  dfrdg2  30443  sltres  30552  nodense  30577  nofulllem5  30594  caures  32047  ssbnd  32078  mapfzcons1  35522  diophrw  35564  eldioph2lem1  35565  eldioph2lem2  35566  rp-imass  36268  fourierdlem93  37927  fouriersw  37959  eldmressn  38381  fnresfnco  38384  afvres  38430