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

Theorem inass 3815
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 680 . . . 4 (((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶) ↔ (𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)))
2 elin 3788 . . . . 5 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
32anbi2i 729 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)))
41, 3bitr4i 267 . . 3 (((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
5 elin 3788 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
65anbi1i 730 . . 3 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶))
7 elin 3788 . . 3 (𝑥 ∈ (𝐴 ∩ (𝐵𝐶)) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
84, 6, 73bitr4i 292 . 2 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐶) ↔ 𝑥 ∈ (𝐴 ∩ (𝐵𝐶)))
98ineqri 3798 1 ((𝐴𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1481  wcel 1988  cin 3566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-in 3574
This theorem is referenced by:  in12  3816  in32  3817  in4  3821  indif2  3862  difun1  3879  dfrab3ss  3897  dfif4  4092  resres  5397  inres  5402  imainrect  5563  predidm  5690  onfr  5751  fresaun  6062  fresaunres2  6063  fimacnvinrn2  6335  epfrs  8592  incexclem  14549  sadeq  15175  smuval2  15185  smumul  15196  ressinbas  15917  ressress  15919  resscatc  16736  sylow2a  18015  ablfac1eu  18453  ressmplbas2  19436  restco  20949  restopnb  20960  kgeni  21321  hausdiag  21429  fclsrest  21809  clsocv  23030  itg2cnlem2  23510  rplogsum  25197  chjassi  28315  pjoml2i  28414  cmcmlem  28420  cmbr3i  28429  fh1  28447  fh2  28448  pj3lem1  29035  dmdbr5  29137  mdslmd3i  29161  mdexchi  29164  atabsi  29230  dmdbr6ati  29252  prsss  29936  inelcarsg  30347  carsgclctunlem1  30353  msrid  31416  osumcllem9N  35069  dihmeetbclemN  36412  dihmeetlem11N  36425  inabs3  39044  uzinico2  39592  caragenuncllem  40489
  Copyright terms: Public domain W3C validator