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

Theorem inass 4048
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 462 . . . 4 (((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶) ↔ (𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)))
2 elin 4023 . . . . 5 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
32anbi2i 616 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)))
41, 3bitr4i 270 . . 3 (((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
5 elin 4023 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
65anbi1i 617 . . 3 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶))
7 elin 4023 . . 3 (𝑥 ∈ (𝐴 ∩ (𝐵𝐶)) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
84, 6, 73bitr4i 295 . 2 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐶) ↔ 𝑥 ∈ (𝐴 ∩ (𝐵𝐶)))
98ineqri 4033 1 ((𝐴𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 386   = wceq 1656  wcel 2164  cin 3797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-in 3805
This theorem is referenced by:  in12  4049  in32  4050  in4  4054  indif2  4100  difun1  4117  dfrab3ss  4134  dfif4  4321  resres  5646  inres  5651  imainrect  5816  predidm  5942  onfr  6002  fresaun  6312  fresaunres2  6313  fimacnvinrn2  6598  epfrs  8884  incexclem  14942  sadeq  15567  smuval2  15577  smumul  15588  ressinbas  16299  ressress  16302  resscatc  17107  sylow2a  18385  ablfac1eu  18826  ressmplbas2  19816  restco  21339  restopnb  21350  kgeni  21711  hausdiag  21819  fclsrest  22198  clsocv  23418  itg2cnlem2  23928  rplogsum  25629  chjassi  28889  pjoml2i  28988  cmcmlem  28994  cmbr3i  29003  fh1  29021  fh2  29022  pj3lem1  29609  dmdbr5  29711  mdslmd3i  29735  mdexchi  29738  atabsi  29804  dmdbr6ati  29826  prsss  30496  inelcarsg  30907  carsgclctunlem1  30913  msrid  31977  redss3  34910  refrelsred4  34914  osumcllem9N  36032  dihmeetbclemN  37372  dihmeetlem11N  37385  inabs3  40034  uzinico2  40577  caragenuncllem  41513
  Copyright terms: Public domain W3C validator