Theorem resundir 5293

Description: Distributive law for restriction over union. (Contributed by NM, 23-Sep-2004.)

Assertion

Ref	Expression
resundir

Proof of Theorem resundir

Step	Hyp	Ref	Expression
1		indir 3745	. 2
2		df-res 5016	. 2
3		df-res 5016	. . 3
4		df-res 5016	. . 3
5	3, 4	uneq12i 3655	. 2
6	1, 2, 5	3eqtr4i 2496	1

Syntax hints:  =wceq 1395  cvv 3109  u.cun 3473  i^icin 3474  X.cxp 5002  |`cres 5006

This theorem is referenced by:  imaundir  5424  fresaunres2  5762  fvunsn  6103  fvsnun1  6106  fvsnun2  6107  fsnunfv  6111  fsnunres  6112  domss2  7696  axdc3lem4  8854  fseq1p1m1  11781  hashgval  12408  hashinf  12410  setsres  14660  setscom  14662  setsid  14673  pwssplit1  17705  constr3pthlem1  24655  ex-res  25162  eulerpartlemt  28310  wfrlem14  29356  mapfzcons1  30649  diophrw  30692  eldioph2lem1  30693  eldioph2lem2  30694  diophin  30706  pwssplit4  31035

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-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  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-v 3111  df-un 3480  df-in 3482  df-res 5016