Theorem dmres 5299

Description: The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
dmres

Proof of Theorem dmres

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3112	. . . . 5
2	1	eldm2 5206	. . . 4
3		19.41v 1771	. . . . 5
4		vex 3112	. . . . . . 7
5	4	opelres 5284	. . . . . 6
6	5	exbii 1667	. . . . 5
7	1	eldm2 5206	. . . . . 6
8	7	anbi1i 695	. . . . 5
9	3, 6, 8	3bitr4i 277	. . . 4
10	2, 9	bitr2i 250	. . 3
11	10	ineqri 3691	. 2
12		incom 3690	. 2
13	11, 12	eqtr3i 2488	1

Syntax hints:  /\wa 369  =wceq 1395  E.wex 1612  e.wcel 1818  i^icin 3474  <.cop 4035  domcdm 5004  |`cres 5006

This theorem is referenced by:  ssdmres  5300  dmresexg  5301  dmressnsn  5317  eldmeldmressn  5319  imadisj  5361  ndmima  5378  imainrect  5453  dmresv  5470  resdmres  5503  coeq0  5521  funimacnv  5665  fnresdisj  5696  fnres  5702  fresaunres2  5762  nfvres  5901  ssimaex  5938  fnreseql  5997  respreima  6016  fveqressseq  6027  ffvresb  6062  fsnunfv  6111  funfvima  6147  funiunfv  6160  offres  6795  fnwelem  6915  ressuppss  6938  ressuppssdif  6940  smores  7042  smores3  7043  smores2  7044  tz7.44-2  7092  tz7.44-3  7093  frfnom  7119  sbthlem5  7651  sbthlem7  7653  domss2  7696  imafi  7833  ordtypelem4  7967  wdomima2g  8033  r0weon  8411  imadomg  8933  dmaddpi  9289  dmmulpi  9290  ltweuz  12072  dmhashres  12414  limsupgle  13300  fvsetsid  14657  setsres  14660  lubdm  15609  glbdm  15622  gsumzaddlem  16934  gsumzaddlemOLD  16936  dprdcntz2  17086  lmres  19801  imacmp  19897  qtoptop2  20200  kqdisj  20233  metreslem  20865  setsmstopn  20981  ismbl  21937  mbfres  22051  dvres3a  22318  cpnres  22340  dvlipcn  22395  dvlip2  22396  c1lip3  22400  dvcnvrelem1  22418  dvcvx  22421  dvlog  23032  cusgrasizeindslem2  24474  eupares  24975  hlimcaui  26154  dfrdg2  29228  sltres  29424  nodense  29449  nofulllem5  29466  caures  30253  ssbnd  30284  mapfzcons1  30649  diophrw  30692  eldioph2lem1  30693  eldioph2lem2  30694  fourierdlem93  31982  fouriersw  32014  eldmressn  32208  fnresfnco  32211  afvres  32257  rp-imass  37795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-xp 5010  df-dm 5014  df-res 5016