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

Theorem inass 3780
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 678 . . . 4 (((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶) ↔ (𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)))
2 elin 3753 . . . . 5 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
32anbi2i 725 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)))
41, 3bitr4i 265 . . 3 (((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
5 elin 3753 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
65anbi1i 726 . . 3 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶))
7 elin 3753 . . 3 (𝑥 ∈ (𝐴 ∩ (𝐵𝐶)) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
84, 6, 73bitr4i 290 . 2 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐶) ↔ 𝑥 ∈ (𝐴 ∩ (𝐵𝐶)))
98ineqri 3763 1 ((𝐴𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 382   = wceq 1474  wcel 1975  cin 3534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-in 3542
This theorem is referenced by:  in12  3781  in32  3782  in4  3786  indif2  3824  difun1  3841  dfrab3ss  3859  dfif4  4046  resres  5312  inres  5317  imainrect  5476  predidm  5601  onfr  5662  fresaun  5969  fresaunres2  5970  fimacnvinrn2  6238  epfrs  8463  incexclem  14349  sadeq  14974  smuval2  14984  smumul  14995  ressinbas  15705  ressress  15707  resscatc  16520  sylow2a  17799  ablfac1eu  18237  ressmplbas2  19218  restco  20716  restopnb  20727  kgeni  21088  hausdiag  21196  fclsrest  21576  clsocv  22771  itg2cnlem2  23248  rplogsum  24929  chjassi  27531  pjoml2i  27630  cmcmlem  27636  cmbr3i  27645  fh1  27663  fh2  27664  pj3lem1  28251  dmdbr5  28353  mdslmd3i  28377  mdexchi  28380  atabsi  28446  dmdbr6ati  28468  prsss  29092  inelcarsg  29502  carsgclctunlem1  29508  msrid  30498  osumcllem9N  34067  dihmeetbclemN  35410  dihmeetlem11N  35423  inabs3  38048  caragenuncllem  39202
  Copyright terms: Public domain W3C validator