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

Theorem inass 4236
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 468 . . . 4 (((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶) ↔ (𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)))
2 elin 3979 . . . . 5 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
32anbi2i 623 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)))
41, 3bitr4i 278 . . 3 (((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
5 elin 3979 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
65anbi1i 624 . . 3 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶))
7 elin 3979 . . 3 (𝑥 ∈ (𝐴 ∩ (𝐵𝐶)) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
84, 6, 73bitr4i 303 . 2 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐶) ↔ 𝑥 ∈ (𝐴 ∩ (𝐵𝐶)))
98ineqri 4220 1 ((𝐴𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1537  wcel 2106  cin 3962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-in 3970
This theorem is referenced by:  in12  4237  in32  4238  in4  4242  indif2  4287  difun1  4305  dfrab3ss  4329  dfif4  4546  resres  6013  inres  6018  imainrect  6203  cnvrescnv  6217  predidm  6349  onfr  6425  fresaun  6780  fresaunres2  6781  fimacnvinrn2  7092  epfrs  9769  incexclem  15869  sadeq  16506  smuval2  16516  smumul  16527  ressinbas  17291  ressress  17294  resscatc  18163  sylow2a  19652  ablfac1eu  20108  ressmplbas2  22063  restco  23188  restopnb  23199  kgeni  23561  hausdiag  23669  fclsrest  24048  clsocv  25298  itg2cnlem2  25812  rplogsum  27586  chjassi  31515  pjoml2i  31614  cmcmlem  31620  cmbr3i  31629  fh1  31647  fh2  31648  pj3lem1  32235  dmdbr5  32337  mdslmd3i  32361  mdexchi  32364  atabsi  32430  dmdbr6ati  32452  prsss  33877  inelcarsg  34293  carsgclctunlem1  34299  msrid  35530  redundss3  38610  refrelsredund4  38614  osumcllem9N  39947  dihmeetbclemN  41287  dihmeetlem11N  41300  inabs3  44996  uzinico2  45515  caragenuncllem  46468  restclsseplem  48711
  Copyright terms: Public domain W3C validator