Theorem dmres 5126

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 2919	. . . . 5 |- x e. _V
2	1	eldm2 5027	. . . 4 |- ( x e. dom ( A |` B ) <-> E. y <. x , y >. e. ( A |` B ) )
3		19.41v 1920	. . . . 5 |- ( E. y ( <. x , y >. e. A /\ x e. B ) <-> ( E. y <. x , y >. e. A /\ x e. B ) )
4		vex 2919	. . . . . . 7 |- y e. _V
5	4	opelres 5110	. . . . . 6 |- ( <. x , y >. e. ( A |` B ) <-> ( <. x , y >. e. A /\ x e. B ) )
6	5	exbii 1589	. . . . 5 |- ( E. y <. x , y >. e. ( A |` B ) <-> E. y ( <. x , y >. e. A /\ x e. B ) )
7	1	eldm2 5027	. . . . . 6 |- ( x e. dom A <-> E. y <. x , y >. e. A )
8	7	anbi1i 677	. . . . 5 |- ( ( x e. dom A /\ x e. B ) <-> ( E. y <. x , y >. e. A /\ x e. B ) )
9	3, 6, 8	3bitr4i 269	. . . 4 |- ( E. y <. x , y >. e. ( A |` B ) <-> ( x e. dom A /\ x e. B ) )
10	2, 9	bitr2i 242	. . 3 |- ( ( x e. dom A /\ x e. B ) <-> x e. dom ( A |` B ) )
11	10	ineqri 3494	. 2 |- ( dom A i^i B ) = dom ( A |` B )
12		incom 3493	. 2 |- ( dom A i^i B ) = ( B i^i dom A )
13	11, 12	eqtr3i 2426	1 |- dom ( A |` B ) = ( B i^i dom A )

Syntax hints:   /\ wa 359   E.wex 1547   = wceq 1649   e. wcel 1721   i^i cin 3279   <.cop 3777   dom cdm 4837   |` cres 4839

This theorem is referenced by:  ssdmres  5127  dmresexg  5128  imadisj  5182  ndmima  5200  imainrect  5271  dmresv  5288  resdmres  5320  funimacnv  5484  fnresdisj  5514  fnres  5520  fresaunres2  5574  nfvres  5719  ssimaex  5747  fnreseql  5799  respreima  5818  ffvresb  5859  fsnunfv  5892  funfvima  5932  funiunfv  5954  offres  6278  fnwelem  6420  smores  6573  smores3  6574  smores2  6575  tz7.44-2  6624  tz7.44-3  6625  frfnom  6651  sbthlem5  7180  sbthlem7  7182  domss2  7225  imafi  7357  ordtypelem4  7446  wdomima2g  7510  r0weon  7850  imadomg  8368  dmaddpi  8723  dmmulpi  8724  ltweuz  11256  limsupgle  12226  setsres  13450  gsumzaddlem  15481  dprdcntz2  15551  lmres  17318  imacmp  17414  qtoptop2  17684  kqdisj  17717  metreslem  18345  setsmstopn  18461  ismbl  19375  mbfres  19489  dvres3a  19754  cpnres  19776  dvlipcn  19831  dvlip2  19832  c1lip3  19836  dvcnvrelem1  19854  dvcvx  19857  dvlog  20495  cusgrasizeindslem2  21436  eupares  21650  hlimcaui  22692  dmhashres  24110  dfrdg2  25366  sltres  25532  nodense  25557  nofulllem5  25574  caures  26356  ssbnd  26387  mapfzcons1  26663  coeq0  26700  diophrw  26707  eldioph2lem1  26708  eldioph2lem2  26709  eldmressn  27851  dmressnsn  27852  fnresfnco  27857  afvres  27903

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-xp 4843  df-dm 4847  df-res 4849