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

Theorem inass 3972
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 459 . . . 4 (((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶) ↔ (𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)))
2 elin 3947 . . . . 5 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
32anbi2i 609 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)))
41, 3bitr4i 267 . . 3 (((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
5 elin 3947 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
65anbi1i 610 . . 3 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶))
7 elin 3947 . . 3 (𝑥 ∈ (𝐴 ∩ (𝐵𝐶)) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
84, 6, 73bitr4i 292 . 2 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐶) ↔ 𝑥 ∈ (𝐴 ∩ (𝐵𝐶)))
98ineqri 3957 1 ((𝐴𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 382   = wceq 1631  wcel 2145  cin 3722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-in 3730
This theorem is referenced by:  in12  3973  in32  3974  in4  3978  indif2  4019  difun1  4036  dfrab3ss  4053  dfif4  4240  resres  5550  inres  5555  imainrect  5716  predidm  5845  onfr  5906  fresaun  6215  fresaunres2  6216  fimacnvinrn2  6492  epfrs  8771  incexclem  14775  sadeq  15402  smuval2  15412  smumul  15423  ressinbas  16143  ressress  16146  resscatc  16962  sylow2a  18241  ablfac1eu  18680  ressmplbas2  19670  restco  21189  restopnb  21200  kgeni  21561  hausdiag  21669  fclsrest  22048  clsocv  23268  itg2cnlem2  23749  rplogsum  25437  chjassi  28685  pjoml2i  28784  cmcmlem  28790  cmbr3i  28799  fh1  28817  fh2  28818  pj3lem1  29405  dmdbr5  29507  mdslmd3i  29531  mdexchi  29534  atabsi  29600  dmdbr6ati  29622  prsss  30302  inelcarsg  30713  carsgclctunlem1  30719  msrid  31780  osumcllem9N  35772  dihmeetbclemN  37114  dihmeetlem11N  37127  inabs3  39745  uzinico2  40307  caragenuncllem  41246
  Copyright terms: Public domain W3C validator