Theorem inass 3707

Description: Associative law for intersection of classes. Exercise 9 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.)

Assertion

Ref	Expression
inass

Proof of Theorem inass

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		anass 649	. . . 4
2		elin 3686	. . . . 5
3	2	anbi2i 694	. . . 4
4	1, 3	bitr4i 252	. . 3
5		elin 3686	. . . 4
6	5	anbi1i 695	. . 3
7		elin 3686	. . 3
8	4, 6, 7	3bitr4i 277	. 2
9	8	ineqri 3691	1

Syntax hints:  /\wa 369  =wceq 1395  e.wcel 1818  i^icin 3474

This theorem is referenced by:  in12  3708  in32  3709  in4  3713  indif2  3740  difun1  3757  dfrab3ss  3775  dfif4  3956  onfr  4922  resres  5291  inres  5296  imainrect  5453  fresaun  5761  fresaunres2  5762  epfrs  8183  incexclem  13648  sadeq  14122  smuval2  14132  smumul  14143  ressinbas  14693  ressress  14694  resscatc  15432  sylow2a  16639  ablfac1eu  17124  ressmplbas2  18117  restco  19665  restopnb  19676  kgeni  20038  hausdiag  20146  fclsrest  20525  clsocv  21690  itg2cnlem2  22169  rplogsum  23712  chjassi  26404  pjoml2i  26503  cmcmlem  26509  cmbr3i  26518  fh1  26536  fh2  26537  pj3lem1  27125  dmdbr5  27227  mdslmd3i  27251  mdexchi  27254  atabsi  27320  dmdbr6ati  27342  fimacnvinrn2  27476  prsss  27898  msrid  28905  predidm  29268  osumcllem9N  35688  dihmeetbclemN  37031  dihmeetlem11N  37044

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-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-in 3482