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

Theorem inass 4227
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 3966 . . . . 5 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
32anbi2i 623 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)))
41, 3bitr4i 278 . . 3 (((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
5 elin 3966 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
65anbi1i 624 . . 3 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶))
7 elin 3966 . . 3 (𝑥 ∈ (𝐴 ∩ (𝐵𝐶)) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
84, 6, 73bitr4i 303 . 2 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐶) ↔ 𝑥 ∈ (𝐴 ∩ (𝐵𝐶)))
98ineqri 4211 1 ((𝐴𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1539  wcel 2107  cin 3949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-in 3957
This theorem is referenced by:  in12  4228  in32  4229  in4  4233  indif2  4280  difun1  4298  dfrab3ss  4322  dfif4  4540  resres  6009  inres  6014  imainrect  6200  cnvrescnv  6214  predidm  6346  onfr  6422  fresaun  6778  fresaunres2  6779  fimacnvinrn2  7091  epfrs  9772  incexclem  15873  sadeq  16510  smuval2  16520  smumul  16531  ressinbas  17292  ressress  17294  resscatc  18155  sylow2a  19638  ablfac1eu  20094  ressmplbas2  22046  restco  23173  restopnb  23184  kgeni  23546  hausdiag  23654  fclsrest  24033  clsocv  25285  itg2cnlem2  25798  rplogsum  27572  chjassi  31506  pjoml2i  31605  cmcmlem  31611  cmbr3i  31620  fh1  31638  fh2  31639  pj3lem1  32226  dmdbr5  32328  mdslmd3i  32352  mdexchi  32355  atabsi  32421  dmdbr6ati  32443  prsss  33916  inelcarsg  34314  carsgclctunlem1  34320  msrid  35551  redundss3  38630  refrelsredund4  38634  osumcllem9N  39967  dihmeetbclemN  41307  dihmeetlem11N  41320  wfac8prim  45024  inabs3  45066  uzinico2  45580  caragenuncllem  46532  resinsn  48778  restclsseplem  48819
  Copyright terms: Public domain W3C validator