Theorem dmres 5128

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 3050	. . . . 5 |- x e. _V
2	1	eldm2 5036	. . . 4 |- ( x e. dom ( A |` B ) <-> E. y <. x , y >. e. ( A |` B ) )
3		19.41v 1832	. . . . 5 |- ( E. y ( <. x , y >. e. A /\ x e. B ) <-> ( E. y <. x , y >. e. A /\ x e. B ) )
4		vex 3050	. . . . . . 7 |- y e. _V
5	4	opelres 5113	. . . . . 6 |- ( <. x , y >. e. ( A |` B ) <-> ( <. x , y >. e. A /\ x e. B ) )
6	5	exbii 1720	. . . . 5 |- ( E. y <. x , y >. e. ( A |` B ) <-> E. y ( <. x , y >. e. A /\ x e. B ) )
7	1	eldm2 5036	. . . . . 6 |- ( x e. dom A <-> E. y <. x , y >. e. A )
8	7	anbi1i 702	. . . . 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 3628	. 2 |- ( dom A i^i B ) = dom ( A |` B )
12		incom 3627	. 2 |- ( dom A i^i B ) = ( B i^i dom A )
13	11, 12	eqtr3i 2477	1 |- dom ( A |` B ) = ( B i^i dom A )

Syntax hints:   /\ wa 371   = wceq 1446   E.wex 1665   e. wcel 1889   i^i cin 3405   <.cop 3976   dom cdm 4837   |` cres 4839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pr 4642

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977  df-br 4406  df-opab 4465  df-xp 4843  df-dm 4847  df-res 4849

This theorem is referenced by:  ssdmres  5129  dmresexg  5130  dmressnsn  5146  eldmeldmressn  5148  imadisj  5190  ndmimaOLD  5209  imainrect  5281  dmresv  5297  resdmres  5329  coeq0  5347  funimacnv  5660  fnresdisj  5691  fnres  5697  fresaunres2  5760  nfvres  5900  ssimaex  5935  fnreseql  5997  respreima  6014  fveqressseq  6023  ffvresb  6059  fsnunfv  6109  funfvima  6145  funiunfv  6158  offres  6793  fnwelem  6916  ressuppss  6939  ressuppssdif  6941  smores  7076  smores3  7077  smores2  7078  tz7.44-2  7130  tz7.44-3  7131  frfnom  7157  sbthlem5  7691  sbthlem7  7693  domss2  7736  imafi  7872  ordtypelem4  8041  wdomima2g  8106  r0weon  8448  imadomg  8967  dmaddpi  9320  dmmulpi  9321  ltweuz  12182  dmhashres  12531  limsupgle  13547  fvsetsid  15160  setsres  15163  lubdm  16237  glbdm  16250  gsumzaddlem  17566  dprdcntz2  17683  lmres  20328  imacmp  20424  qtoptop2  20726  kqdisj  20759  metreslem  21389  setsmstopn  21505  ismbl  22492  mbfres  22612  dvres3a  22881  cpnres  22903  dvlipcn  22958  dvlip2  22959  c1lip3  22963  dvcnvrelem1  22981  dvcvx  22984  dvlog  23608  cusgrasizeindslem2  25214  eupares  25715  hlimcaui  26901  dfrdg2  30454  sltres  30563  nodense  30590  nofulllem5  30607  caures  32101  ssbnd  32132  mapfzcons1  35571  diophrw  35613  eldioph2lem1  35614  eldioph2lem2  35615  rp-imass  36378  fourierdlem93  38073  fouriersw  38105  eldmressn  38634  fnresfnco  38637  afvres  38684  uhgrspansubgrlem  39372