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 2973	. . . . 5 |- x e. _V
2	1	eldm2 5034	. . . 4 |- ( x e. dom ( A |` B ) <-> E. y <. x , y >. e. ( A |` B ) )
3		19.41v 1924	. . . . 5 |- ( E. y ( <. x , y >. e. A /\ x e. B ) <-> ( E. y <. x , y >. e. A /\ x e. B ) )
4		vex 2973	. . . . . . 7 |- y e. _V
5	4	opelres 5112	. . . . . 6 |- ( <. x , y >. e. ( A |` B ) <-> ( <. x , y >. e. A /\ x e. B ) )
6	5	exbii 1639	. . . . 5 |- ( E. y <. x , y >. e. ( A |` B ) <-> E. y ( <. x , y >. e. A /\ x e. B ) )
7	1	eldm2 5034	. . . . . 6 |- ( x e. dom A <-> E. y <. x , y >. e. A )
8	7	anbi1i 690	. . . . 5 |- ( ( x e. dom A /\ x e. B ) <-> ( E. y <. x , y >. e. A /\ x e. B ) )
9	3, 6, 8	3bitr4i 277	. . . 4 |- ( E. y <. x , y >. e. ( A |` B ) <-> ( x e. dom A /\ x e. B ) )
10	2, 9	bitr2i 250	. . 3 |- ( ( x e. dom A /\ x e. B ) <-> x e. dom ( A |` B ) )
11	10	ineqri 3541	. 2 |- ( dom A i^i B ) = dom ( A |` B )
12		incom 3540	. 2 |- ( dom A i^i B ) = ( B i^i dom A )
13	11, 12	eqtr3i 2463	1 |- dom ( A |` B ) = ( B i^i dom A )

Syntax hints:   /\ wa 369   = wceq 1364   E.wex 1591   e. wcel 1761   i^i cin 3324   <.cop 3880   dom cdm 4836   |` cres 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pr 4528

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-br 4290  df-opab 4348  df-xp 4842  df-dm 4846  df-res 4848

This theorem is referenced by:  ssdmres  5129  dmresexg  5130  imadisj  5185  ndmima  5202  imainrect  5276  dmresv  5293  resdmres  5326  funimacnv  5487  fnresdisj  5518  fnres  5524  fresaunres2  5580  nfvres  5717  ssimaex  5753  fnreseql  5810  respreima  5829  ffvresb  5871  fsnunfv  5915  funfvima  5949  funiunfv  5962  offres  6571  fnwelem  6686  ressuppss  6707  ressuppssdif  6709  smores  6809  smores3  6810  smores2  6811  tz7.44-2  6859  tz7.44-3  6860  frfnom  6886  sbthlem5  7421  sbthlem7  7423  domss2  7466  imafi  7600  ordtypelem4  7731  wdomima2g  7797  r0weon  8175  imadomg  8697  dmaddpi  9055  dmmulpi  9056  ltweuz  11780  dmhashres  12108  limsupgle  12951  fvsetsid  14195  setsres  14198  lubdm  15145  glbdm  15158  gsumzaddlem  16401  gsumzaddlemOLD  16403  dprdcntz2  16526  lmres  18863  imacmp  18959  qtoptop2  19231  kqdisj  19264  metreslem  19896  setsmstopn  20012  ismbl  20968  mbfres  21081  dvres3a  21348  cpnres  21370  dvlipcn  21425  dvlip2  21426  c1lip3  21430  dvcnvrelem1  21448  dvcvx  21451  dvlog  22055  cusgrasizeindslem2  23317  eupares  23531  hlimcaui  24574  gsumle  26181  dfrdg2  27538  sltres  27734  nodense  27759  nofulllem5  27776  caures  28581  ssbnd  28612  mapfzcons1  28978  coeq0  29015  diophrw  29022  eldioph2lem1  29023  eldioph2lem2  29024  eldmressn  29952  dmressnsn  29953  fnresfnco  29957  afvres  30003  eldmeldmressn  30065