Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  inass Structured version   Visualization version   GIF version

Theorem inass 3785
 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.
StepHypRef Expression
1 anass 679 . . . 4 (((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶) ↔ (𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)))
2 elin 3758 . . . . 5 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
32anbi2i 726 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)))
41, 3bitr4i 266 . . 3 (((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
5 elin 3758 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
65anbi1i 727 . . 3 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶))
7 elin 3758 . . 3 (𝑥 ∈ (𝐴 ∩ (𝐵𝐶)) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
84, 6, 73bitr4i 291 . 2 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐶) ↔ 𝑥 ∈ (𝐴 ∩ (𝐵𝐶)))
98ineqri 3768 1 ((𝐴𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ∩ cin 3539 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547 This theorem is referenced by:  in12  3786  in32  3787  in4  3791  indif2  3829  difun1  3846  dfrab3ss  3864  dfif4  4051  resres  5329  inres  5334  imainrect  5494  predidm  5619  onfr  5680  fresaun  5988  fresaunres2  5989  fimacnvinrn2  6257  epfrs  8490  incexclem  14407  sadeq  15032  smuval2  15042  smumul  15053  ressinbas  15763  ressress  15765  resscatc  16578  sylow2a  17857  ablfac1eu  18295  ressmplbas2  19276  restco  20778  restopnb  20789  kgeni  21150  hausdiag  21258  fclsrest  21638  clsocv  22857  itg2cnlem2  23335  rplogsum  25016  chjassi  27729  pjoml2i  27828  cmcmlem  27834  cmbr3i  27843  fh1  27861  fh2  27862  pj3lem1  28449  dmdbr5  28551  mdslmd3i  28575  mdexchi  28578  atabsi  28644  dmdbr6ati  28666  prsss  29290  inelcarsg  29700  carsgclctunlem1  29706  msrid  30696  osumcllem9N  34268  dihmeetbclemN  35611  dihmeetlem11N  35624  inabs3  38249  caragenuncllem  39402
 Copyright terms: Public domain W3C validator