Theorem inass 2226

Description: Associative law for intersection of classes. Exercise 9 of [TakeutiZaring] p. 17.

Assertion

Ref	Expression
inass	|- ((A i^i B) i^i C) = (A i^i (B i^i C))

Proof of Theorem inass

Step	Hyp	Ref	Expression
1		anass 441	. . . 4 |- (((x e. A /\ x e. B) /\ x e. C) <-> (x e. A /\ (x e. B /\ x e. C)))
2		elin 2210	. . . . 5 |- (x e. (B i^i C) <-> (x e. B /\ x e. C))
3	2	anbi2i 482	. . . 4 |- ((x e. A /\ x e. (B i^i C)) <-> (x e. A /\ (x e. B /\ x e. C)))
4	1, 3	bitr4 176	. . 3 |- (((x e. A /\ x e. B) /\ x e. C) <-> (x e. A /\ x e. (B i^i C)))
5		elin 2210	. . . 4 |- (x e. (A i^i B) <-> (x e. A /\ x e. B))
6	5	anbi1i 483	. . 3 |- ((x e. (A i^i B) /\ x e. C) <-> ((x e. A /\ x e. B) /\ x e. C))
7		elin 2210	. . 3 |- (x e. (A i^i (B i^i C)) <-> (x e. A /\ x e. (B i^i C)))
8	4, 6, 7	3bitr4 183	. 2 |- ((x e. (A i^i B) /\ x e. C) <-> x e. (A i^i (B i^i C)))
9	8	ineqri 2212	1 |- ((A i^i B) i^i C) = (A i^i (B i^i C))

Syntax hints:   /\ wa 223   = wceq 958   e. wcel 960   i^i cin 2049

This theorem is referenced by:  in12 2227  in23 2228  in4 2229  difun1 2266  onfr 2992  resres 3383  resdisj 3477  rescnvcnv 3499  zfregs 4657  chjass 9404  pjoml2 9523  cmcmlem 9529  cmbr3 9538  fh1t 9556  fh2t 9557  pj3lem1 10129  dmdbr5 10230  mdslmd3 10254  mdexch 10257  atabs 10323  dmdbr6at 10345

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-in 2054

Copyright terms: Public domain